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