Agda.TypeChecking.Implicit
Description
Functions for inserting implicit arguments at the right places.
- data ImplicitInsertion
- impInsert :: Int -> ImplicitInsertion
- insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion
Documentation
data ImplicitInsertion Source
Constructors
| ImpInsert Int | 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
insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertionSource
The list should be non-empty.