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
- Std.Tactic.noFun = Lean.ParserDescr.node `Std.Tactic.noFun 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "fun") (Lean.ParserDescr.symbol "."))
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
- Std.Tactic.«termλ.» = Lean.ParserDescr.node `Std.Tactic.termλ. 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "λ") (Lean.ParserDescr.symbol "."))
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.