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

Safe HaskellNone

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 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 :: Int -> (Hiding -> String -> Bool) -> Type -> TCM (NamedArgs, Type)Source

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.

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 String

bad named argument

NoInsertNeeded 

insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertionSource

The list should be non-empty.