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

def Batteries.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 Batteries.Tactic.funDot : Lean.ParserDescr

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

Equations

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

def Batteries.Tactic.lambdaDot : Lean.ParserDescr

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

Equations

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

def Batteries.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 Batteries.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.