Documentation

Lean.Parser

@[export lean_mk_antiquot_parenthesizer]

def Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : optParam Bool true) (isPseudoKind : optParam Bool true) :

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer name kind anonymous isPseudoKind = Lean.Parser.mkAntiquot.parenthesizer name kind anonymous isPseudoKind

def Lean.PrettyPrinter.Parenthesizer.ident.parenthesizer:

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.ident.parenthesizer = Lean.Parser.Term.ident.parenthesizer

def Lean.PrettyPrinter.Parenthesizer.numLit.parenthesizer:

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.numLit.parenthesizer = Lean.Parser.Term.num.parenthesizer

def Lean.PrettyPrinter.Parenthesizer.scientificLit.parenthesizer:

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.scientificLit.parenthesizer = Lean.Parser.Term.scientific.parenthesizer

def Lean.PrettyPrinter.Parenthesizer.charLit.parenthesizer:

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.charLit.parenthesizer = Lean.Parser.Term.char.parenthesizer

def Lean.PrettyPrinter.Parenthesizer.strLit.parenthesizer:

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.PrettyPrinter.Parenthesizer.strLit.parenthesizer = Lean.Parser.Term.str.parenthesizer

@[export lean_pretty_printer_parenthesizer_interpret_parser_descr]

unsafe def Lean.PrettyPrinter.Parenthesizer.interpretParserDescr:

Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Parenthesizer

Equations

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

@[export lean_mk_antiquot_formatter]

def Lean.PrettyPrinter.Formatter.mkAntiquot.formatter (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : optParam Bool true) (isPseudoKind : optParam Bool true) :

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.mkAntiquot.formatter name kind anonymous isPseudoKind = Lean.Parser.mkAntiquot.formatter name kind anonymous isPseudoKind

def Lean.PrettyPrinter.Formatter.ident.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.ident.formatter = Lean.Parser.Term.ident.formatter

def Lean.PrettyPrinter.Formatter.numLit.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.numLit.formatter = Lean.Parser.Term.num.formatter

def Lean.PrettyPrinter.Formatter.scientificLit.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.scientificLit.formatter = Lean.Parser.Term.scientific.formatter

def Lean.PrettyPrinter.Formatter.charLit.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.charLit.formatter = Lean.Parser.Term.char.formatter

def Lean.PrettyPrinter.Formatter.strLit.formatter:

Lean.PrettyPrinter.Formatter

Equations

Lean.PrettyPrinter.Formatter.strLit.formatter = Lean.Parser.Term.str.formatter

@[export lean_pretty_printer_formatter_interpret_parser_descr]

unsafe def Lean.PrettyPrinter.Formatter.interpretParserDescr:

Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Formatter

Equations

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