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

Instances For

source
def Lean.PrettyPrinter.Parenthesizer.ident.parenthesizer :
Parenthesizer
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.PrettyPrinter.Parenthesizer.strLit.parenthesizer :
Parenthesizer
Equations

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

Instances For

source
@[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.unicodeSymbol tk asciiTk preserve) = pure (Lean.Parser.unicodeSymbol.parenthesizer tk asciiTk preserve)
- 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)

Instances For

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

Instances For

source
def Lean.PrettyPrinter.Formatter.ident.formatter :
Formatter
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.PrettyPrinter.Formatter.strLit.formatter :
Formatter
Equations

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

Instances For

source
@[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.unicodeSymbol tk asciiTk preserve) = pure (Lean.Parser.unicodeSymbol.formatter tk asciiTk preserve)
- 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)

Instances For