Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

- implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)
- data ImplicitInsertion
  - = ImpInsert [Hiding]
  - | BadImplicits
  - | NoSuchName String
  - | NoInsertNeeded
- impInsert :: [Hiding] -> ImplicitInsertion
- insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion

# Documentation

implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)

`implicitArgs n expand t` generates up to `n` implicit arguments metas (unbounded if `n<0`), as long as `t` is a function type and `expand` holds on the hiding info of its domain.

data ImplicitInsertion

Constructors

ImpInsert [Hiding] | this many implicits have to be inserted
BadImplicits | hidden argument where there should have been a non-hidden arg
NoSuchName String | bad named argument
NoInsertNeeded |

Instances

Show ImplicitInsertion |

impInsert :: [Hiding] -> ImplicitInsertion

insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion

The list should be non-empty.