def term𝒞 : Lean.ParserDescr

Equations

• term𝒞 = Lean.ParserDescr.node `term𝒞 1024 (Lean.ParserDescr.symbol "𝒞")

def termHull : Lean.ParserDescr

Equations

• termHull = Lean.ParserDescr.node `termHull 1024 (Lean.ParserDescr.symbol "hull")

def termD : Lean.ParserDescr

Equations

• termD = Lean.ParserDescr.node `termD 1024 (Lean.ParserDescr.symbol "D")

def termSmooth_on : Lean.ParserDescr

Equations

• termSmooth_on = Lean.ParserDescr.node `termSmooth_on 1024 (Lean.ParserDescr.symbol "smooth_on")

def «term∀ᶠ_Near_,_» : Lean.ParserDescr

Equations

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

def «term_⬝_» : Lean.TrailingParserDescr

Equations

• «term_⬝_» = Lean.ParserDescr.trailingNode `«term_⬝_» 70 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ ") (Lean.ParserDescr.cat `term 65))