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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

Documentation

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

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 eti is ExplicitToInstance, then explicit arguments are considered as instance arguments.

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

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 eti is ExplicitToInstance, then explicit arguments are considered as instance arguments.

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 ArgName

bad named argument

NoInsertNeeded 

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

The list should be non-empty.