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

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

# Documentation

Arguments

 :: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m) => 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. -> m (Args, Type) The eliminating arguments and the remaining type.

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

Arguments

 :: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m) => 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. -> m (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.

Arguments

 :: MonadMetaSolver m => ArgInfo Kind/relevance of meta. -> ArgName Name suggestion for meta. -> Comparison Check (CmpLeq) or infer (CmpEq) the type. -> Type Type of meta. -> m (MetaId, Term) The created meta as id and as term.

Create a metavariable according to the Hiding info.

Arguments

 :: ArgInfo Kind/relevance of meta. -> ArgName Name suggestion for meta. -> Comparison Check (CmpLeq) or infer (CmpEq) the type. -> Type Type of meta. -> TCM (MetaId, Term) The created meta as id and as term.

Create a questionmark according to the Hiding info.

Possible results of insertImplicit.

Constructors

 ImpInsert [Dom ()] 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
 Source # Instance detailsDefined in Agda.TypeChecking.Implicit MethodsshowList :: [ImplicitInsertion] -> ShowS #

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.

Arguments

 :: NamedArg e Next given argument a. -> [Dom 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.