def «term_≫_» : Lean.TrailingParserDescr

Equations

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

def «term_≪_» : Lean.TrailingParserDescr

Equations

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