@[export lean_mk_antiquot_parenthesizer]

def Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous isPseudoKind : Bool := true) : 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 : Parenthesizer

Equations

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

def Lean.PrettyPrinter.Parenthesizer.numLit.parenthesizer : Parenthesizer

Equations

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

def Lean.PrettyPrinter.Parenthesizer.scientificLit.parenthesizer : Parenthesizer

Equations

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

def Lean.PrettyPrinter.Parenthesizer.charLit.parenthesizer : Parenthesizer

Equations

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

def Lean.PrettyPrinter.Parenthesizer.strLit.parenthesizer : 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 : ParserDescr → CoreM Parenthesizer

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Parenthesizer.interpretParserDescr (Lean.ParserDescr.const n) = liftM (Lean.Parser.getConstAlias Lean.PrettyPrinter.Parenthesizer.parenthesizerAliasesRef n)
• Lean.PrettyPrinter.Parenthesizer.interpretParserDescr (Lean.ParserDescr.symbol tk) = pure (Lean.Parser.symbol.parenthesizer tk)
• Lean.PrettyPrinter.Parenthesizer.interpretParserDescr (Lean.ParserDescr.nonReservedSymbol tk includeIdent) = pure (Lean.Parser.nonReservedSymbol.parenthesizer tk includeIdent)
• Lean.PrettyPrinter.Parenthesizer.interpretParserDescr (Lean.ParserDescr.parser constName) = Lean.PrettyPrinter.combinatorParenthesizerAttribute.runDeclFor constName
• Lean.PrettyPrinter.Parenthesizer.interpretParserDescr (Lean.ParserDescr.cat catName prec) = pure (Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer catName prec)

@[export lean_mk_antiquot_formatter]

def Lean.PrettyPrinter.Formatter.mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous isPseudoKind : Bool := true) : 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 : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.numLit.formatter : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.scientificLit.formatter : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.charLit.formatter : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.strLit.formatter : 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 : ParserDescr → CoreM Formatter

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Formatter.interpretParserDescr (Lean.ParserDescr.const n) = liftM (Lean.Parser.getConstAlias Lean.PrettyPrinter.Formatter.formatterAliasesRef n)
• Lean.PrettyPrinter.Formatter.interpretParserDescr (Lean.ParserDescr.symbol tk) = pure (Lean.Parser.symbol.formatter tk)
• Lean.PrettyPrinter.Formatter.interpretParserDescr (Lean.ParserDescr.nonReservedSymbol tk includeIdent) = pure (Lean.Parser.nonReservedSymbol.formatter tk)
• Lean.PrettyPrinter.Formatter.interpretParserDescr (Lean.ParserDescr.parser constName) = Lean.PrettyPrinter.combinatorFormatterAttribute.runDeclFor constName
• Lean.PrettyPrinter.Formatter.interpretParserDescr (Lean.ParserDescr.cat catName prec) = pure (Lean.PrettyPrinter.Formatter.categoryParser.formatter catName)