Deprecation warnings for match ⋯ with., fun., λ., and intro..

def Std.Tactic.matchWithDot : Lean.ParserDescr

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

Equations

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

def Std.Tactic.funDot : Lean.ParserDescr

The syntax fun. has been deprecated in favor of nofun.

Equations

• Std.Tactic.funDot = Lean.ParserDescr.node `Std.Tactic.funDot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "fun") (Lean.ParserDescr.symbol "."))

def Std.Tactic.lambdaDot : Lean.ParserDescr

The syntax λ. has been deprecated in favor of nofun.

Equations

• Std.Tactic.lambdaDot = Lean.ParserDescr.node `Std.Tactic.lambdaDot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "fun") (Lean.ParserDescr.symbol "."))

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

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

Equations

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

def Std.Tactic.introDot : Lean.ParserDescr

The syntax intro. is deprecated in favor of nofun.

Equations

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