Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

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

matchPattern :: MonadTCM tcm => Arg Pattern -> Arg Term -> tcm (Match, Arg Term)