| Safe Haskell | None |
|---|
Agda.TypeChecking.Implicit
Description
Functions for inserting implicit arguments at the right places.
- 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)Source
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 Source
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
impInsert :: [Hiding] -> ImplicitInsertionSource
insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertionSource
The list should be non-empty.