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.

def Std.Tactic.noMatch : Lean.ParserDescr

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.

def Std.Tactic.elabNoMatch' : Lean.Elab.Term.TermElab

Elaborator for match x with.

def Std.Tactic.noFun : Lean.ParserDescr

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.

def Std.Tactic.«termλ.» : Lean.ParserDescr

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.

def Std.Tactic.«tacticMatch_,,With.» : Lean.ParserDescr

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.

def Std.Tactic.«tacticIntro.» : Lean.ParserDescr

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.