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

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.

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

 Source # MethodsshowList :: [ImplicitInsertion] -> ShowS #

The list should be non-empty.