def «term_#__» : Lean.TrailingParserDescr

Equations

• «term_#__» = Lean.ParserDescr.trailingNode `«term_#__» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " #") (Lean.ParserDescr.const `ws))) (Lean.ParserDescr.cat `term 10))

def «term_##__» : Lean.TrailingParserDescr

Equations

• «term_##__» = Lean.ParserDescr.trailingNode `«term_##__» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ##") (Lean.ParserDescr.const `ws))) (Lean.ParserDescr.cat `term 10))

def tacticNm___ : Lean.ParserDescr

Equations

• tacticNm___ = Lean.ParserDescr.node `tacticNm___ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "nm " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `ppSpace) (Lean.ParserDescr.const `colGt)) Lean.binderIdent)))

def «termτ_,_» : Lean.ParserDescr

Equations

• «termτ_,_» = Lean.ParserDescr.node `«termτ_,_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "τ") Lean.explicitBinders) (Lean.ParserDescr.symbol ", ")) (Lean.ParserDescr.cat `term 0))