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.