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

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

Documentation

insertImplicitProblem :: Problem -> TCM ProblemSource

Insert implicit patterns in a problem.

insertImplicitPatterns :: [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]Source

Insert implicit patterns in a list of patterns.