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

Safe HaskellNone

Agda.TypeChecking.Patterns.Match

Synopsis

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

matchPatterns :: [Arg Pattern] -> [Arg Term] -> TCM (Match, [Arg Term])Source

matchPattern :: Arg Pattern -> Arg Term -> TCM (Match, Arg Term)Source