Documentation

Std.Tactic.NoMatch

This adds support for the alternative syntax match x with. instead of nomatch x. It is more powerful because it supports pattern matching on multiple discriminants, like regular match, and simply has no alternatives in the match.

Along the same lines, fun. is a nullary pattern matching function; it is equivalent to fun x y z => match x, y, z with. where all variables are introduced in order to find an impossible pattern. The match x with. and intro. tactics do the same thing but in tactic mode.

The syntax match x with. is a variant of nomatch x which supports pattern matching on multiple discriminants, like regular match, and simply has no alternatives in the match.

Equations
  • One or more equations did not get rendered due to their size.

Elaborator for match x with.

Equations
  • One or more equations did not get rendered due to their size.

The syntax fun. or λ. (dot required) is shorthand for an empty pattern match function, i.e. fun x y z => match x, y, z with. for an appropriate number of arguments.

Equations

The syntax fun. or λ. (dot required) is shorthand for an empty pattern match function, i.e. fun x y z => match x, y, z with. for an appropriate number of arguments.

Equations

The syntax match x with. is a variant of nomatch x which supports pattern matching on multiple discriminants, like regular match, and simply has no alternatives in the match.

Equations
  • One or more equations did not get rendered due to their size.

The tactic intro. is shorthand for exact fun.: it introduces the assumptions, then performs an empty pattern match, closing the goal if the introduced pattern is impossible.

Equations
  • One or more equations did not get rendered due to their size.