def «term_<$_» : Lean.TrailingParserDescr

Equations

• «term_<$_» = Lean.ParserDescr.trailingNode `«term_<$_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$ ") (Lean.ParserDescr.cat `term 101))

def doElemDiscard_ : Lean.ParserDescr

discard e is a synonym for let _ ← e in a do block.

Equations

• doElemDiscard_ = Lean.ParserDescr.node `doElemDiscard_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "discard ") (Lean.ParserDescr.cat `term 0))

def default : Lean.Parser.Parser

Equations

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

def termTodo!__ : Lean.ParserDescr

A shorthand to indicate at runtime that something has not been implemented yet. A (default := e) can be given as first argument to indicate the value to be returned, when either no Inhabited instance exists for the return type, or one exists but returns a nonsensical value for this purpose.

Equations

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