Pattern matching

Pattern matching over terms

match%match-key term-scrutinee with term-case+

match-key::=rocq|lazy|multiterm-scrutinee::=ocaml-expr|string|constr-quotationterm-case::=| term-pattern -> ocaml-exprterm-pattern::=pattern|Context pattern as ident?pattern::={| cpattern |}|_

Matches the term term-scrutinee, of type constr, against any of the term-case in order.

In a branch, a pattern variable ?x is bound to an OCaml variable named x of type constr. When a match is found, x contains the value of the matched variable ?x.

If a branch fails, matching may continue with later branches depending on match-key.

As in Ltac, matching is non-linear, i.e., pattern variables that occur more than once must be syntactically equal or be α-convertible.

match%lazy

Non-backtracking match: if a branch fails, the match is exited. In other words, match%lazy commits to the first matching branch.

match%rocq

Backtracking match: if a branch fails, the next branch is tried.

match%multi

Multi-success match: behaves like match%rocq, except that a failure after the match also backtracks to the next branch.

Context pattern as ident?

Matches a subterm instead of the whole term (equivalent to Ltac’s context ident [ pattern ]). If ident is specified, the context is bound to an OCaml variable of the same name in the branch.

Pattern matching over goals

match%match-key reverse? goal with goal-case+

goal-case::=| goal-pattern -> ocaml-exprgoal-pattern::=hypotheses-pattern , term-patternhypotheses-pattern::={ hypothesis-pattern*; }|_hypothesis-pattern::=ident = term-pattern|ident = term-pattern :: term-pattern

Matches the current goal against any of the goal-pattern.

reverse?

If reverse is specified, hypotheses are matched in the reverse order.

goal-pattern

Specifies how to match the goal’s hypotheses and conclusion.

hypothesis-pattern

Matches a single hypothesis.

ident = term-pattern

Matches the body of the hypothesis against term-pattern. If term-pattern is _, matching succeeds regardless of whether the hypothesis has a body or not.

Warning

Do not confuse _ with {|_|}: the former matches any hypothesis, while the latter matches only if the hypothesis has a body (regardless of the body).

ident = term-pattern :: term-pattern

Matches the body and type of the hypothesis against term-pattern.