| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

insertImplicitProblem :: Problem -> TCM Problem
insertImplicitPatterns :: [NamedArg Pattern] -> Telescope -> TCM [NamedArg Pattern]

Documentation

insertImplicitProblem :: Problem -> TCM Problem | Source

Insert implicit patterns in a problem.

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

Insert implicit patterns in a list of patterns.
Produced by Haddock version 2.4.2