Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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.1