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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.