Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

Documentation

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

implicitArgs n expand eti 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.

If explicit arguments are to be inserted as well, they are inserted as instance arguments (used for recursive instance search).

implicitNamedArgs :: Int -> (Hiding -> ArgName -> Bool) -> Type -> TCM (NamedArgs, Type)

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

If explicit arguments are to be inserted as well, they are inserted as instance arguments (used for recursive instance search).

newMetaArg

Arguments

:: ArgInfo

Kind/relevance of meta.

-> ArgName

Name suggestion for meta.

-> Type

Type of meta.

-> TCM (MetaId, Term)

The created meta as id and as term.

Create a metavariable according to the Hiding info.

newInteractionMetaArg

Arguments

:: ArgInfo

Kind/relevance of meta.

-> ArgName

Name suggestion for meta.

-> Type

Type of meta.

-> TCM (MetaId, Term)

The created meta as id and as term.

Create a questionmark according to the Hiding info.

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 ArgName

bad named argument

NoInsertNeeded

Instances

Show ImplicitInsertion

Methods

showsPrec :: Int -> ImplicitInsertion -> ShowS

show :: ImplicitInsertion -> String

showList :: [ImplicitInsertion] -> ShowS

impInsert :: [Hiding] -> ImplicitInsertion

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

The list should be non-empty.