Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.CompiledClause.Match
Documentation
matchCompiled
::
CompiledClauses
->
MaybeReducedArgs
->
TCM
(
Reduced
(
Blocked
Args
)
Term
)
Source
type
Stack
= [(
CompiledClauses
,
MaybeReducedArgs
,
Args
->
Args
)]
Source
match
::
CompiledClauses
->
MaybeReducedArgs
-> (
Args
->
Args
) ->
Stack
->
TCM
(
Reduced
(
Blocked
Args
)
Term
)
Source
match'
::
Stack
->
TCM
(
Reduced
(
Blocked
Args
)
Term
)
Source
Produced by
Haddock
version 2.6.1