Agda-2.3.0: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Patterns.Match
Synopsis
data Match Source
If matching is inconclusive (DontKnow) we want to know whether it is due to a particular meta variable.
DontKnow
Constructors
Instances
matchPatterns :: [Arg Pattern] -> [Arg Term] -> TCM (Match, [Arg Term])Source
matchPattern :: Arg Pattern -> Arg Term -> TCM (Match, Arg Term)Source