Agda-2.2.10: 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.6.1