| 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) |

Instances

Monoid Match

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.4.2