Safe Haskell | None |
---|
Agda.TypeChecking.Rules.LHS.Implicit
- insertImplicitProblem :: Problem -> TCM Problem
- insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
Documentation
insertImplicitProblem :: Problem -> TCM Problem
Insert implicit patterns in a problem.
insertImplicitPatterns :: ExpandHidden -> [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]
Insert implicit patterns in a list of patterns.