Agda-2.3.0.1: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Rules.LHS.Implicit
Synopsis
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.