Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

Documentation

implicitArgs

Arguments

:: Int

n, the maximum number of implicts to be inserted.

-> (Hiding -> Bool)

expand, the predicate to test whether we should keep inserting.

-> Type

The (function) type t we are eliminating.

-> TCM (Args, Type)

The eliminating arguments and the remaining 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.

implicitNamedArgs

Arguments

:: Int

n, the maximum number of implicts to be inserted.

-> (Hiding -> ArgName -> Bool)

expand, the predicate to test whether we should keep inserting.

-> Type

The (function) type t we are eliminating.

-> TCM (NamedArgs, Type)

The eliminating arguments and the remaining type.

implicitNamedArgs n expand 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.

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

Possible results of insertImplicit.

Constructors

ImpInsert [Hiding]

Success: this many implicits have to be inserted (list can be empty).

BadImplicits

Error: hidden argument where there should have been a non-hidden argument.

NoSuchName ArgName

Error: bad named argument.

Instances

Show ImplicitInsertion

Defined in Agda.TypeChecking.Implicit

Methods

showsPrec :: Int -> ImplicitInsertion -> ShowS

show :: ImplicitInsertion -> String

showList :: [ImplicitInsertion] -> ShowS

pattern NoInsertNeeded :: ImplicitInsertion

insertImplicit

Arguments

:: NamedArg e

Next given argument a.

-> [Dom a]

Expected arguments ts.

-> ImplicitInsertion

If the next given argument is a and the expected arguments are ts insertImplicit' a ts returns the prefix of ts that precedes a.

If a is named but this name does not appear in ts, the NoSuchName exception is thrown.

insertImplicit'

Arguments

:: NamedArg e

Next given argument a.

-> [Arg ArgName]

Expected arguments ts.

-> ImplicitInsertion

If the next given argument is a and the expected arguments are ts insertImplicit' a ts returns the prefix of ts that precedes a.

If a is named but this name does not appear in ts, the NoSuchName exception is thrown.