Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Patterns.Match
Synopsis
data
Match
=
Yes
[
Term
]
|
No
|
DontKnow
(
Maybe
MetaId
)
matchPatterns
::
MonadTCM
tcm => [
Arg
Pattern
] -> [
Arg
Term
] -> tcm (
Match
, [
Arg
Term
])
matchPattern
::
MonadTCM
tcm =>
Arg
Pattern
->
Arg
Term
-> tcm (
Match
,
Arg
Term
)
Documentation
data
Match
Source
If matching is inconclusive (
DontKnow
) we want to know whether it is due to a particular meta variable.
Constructors
Yes
[
Term
]
No
DontKnow
(
Maybe
MetaId
)
matchPatterns
::
MonadTCM
tcm => [
Arg
Pattern
] -> [
Arg
Term
] -> tcm (
Match
, [
Arg
Term
])
Source
matchPattern
::
MonadTCM
tcm =>
Arg
Pattern
->
Arg
Term
-> tcm (
Match
,
Arg
Term
)
Source
Produced by
Haddock
version 2.6.0