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

Safe Haskell | None

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

- 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.