@[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

@[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