def
Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer
(name : String)
(kind : Option Lean.SyntaxNodeKind)
(anonymous : optParam Bool true)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer name kind anonymous = Lean.Parser.mkAntiquot.parenthesizer name kind anonymous
Equations
- Lean.PrettyPrinter.Parenthesizer.interpretParserDescr x = match x with | Lean.ParserDescr.const n => liftM (Lean.Parser.getConstAlias Lean.PrettyPrinter.Parenthesizer.parenthesizerAliasesRef n) | Lean.ParserDescr.unary n d => do let a ← liftM (Lean.Parser.getUnaryAlias Lean.PrettyPrinter.Parenthesizer.parenthesizerAliasesRef n) let a_1 ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d pure (a a_1) | Lean.ParserDescr.binary n d₁ d₂ => do let a ← liftM (Lean.Parser.getBinaryAlias Lean.PrettyPrinter.Parenthesizer.parenthesizerAliasesRef n) let a_1 ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d₁ let a_2 ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d₂ pure (a a_1 a_2) | Lean.ParserDescr.node k prec d => do let a ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d pure (Lean.PrettyPrinter.Parenthesizer.leadingNode.parenthesizer k prec a) | Lean.ParserDescr.nodeWithAntiquot x k d => do let a ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d pure (Lean.PrettyPrinter.Parenthesizer.node.parenthesizer k a) | Lean.ParserDescr.sepBy p sep psep trail => do let a ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr p let a_1 ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr psep pure (Lean.Parser.sepBy.parenthesizer a sep a_1 trail) | Lean.ParserDescr.sepBy1 p sep psep trail => do let a ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr p let a_1 ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr psep pure (Lean.Parser.sepBy1.parenthesizer a sep a_1 trail) | Lean.ParserDescr.trailingNode k prec lhsPrec d => do let a ← Lean.PrettyPrinter.Parenthesizer.interpretParserDescr d pure (Lean.PrettyPrinter.Parenthesizer.trailingNode.parenthesizer k prec lhsPrec a) | Lean.ParserDescr.symbol tk => pure (Lean.Parser.symbol.parenthesizer tk) | Lean.ParserDescr.nonReservedSymbol tk includeIdent => pure (Lean.Parser.nonReservedSymbol.parenthesizer tk includeIdent) | Lean.ParserDescr.parser constName => Lean.ParserCompiler.CombinatorAttribute.runDeclFor Lean.PrettyPrinter.combinatorParenthesizerAttribute constName | Lean.ParserDescr.cat catName prec => pure (Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer catName prec)
def
Lean.PrettyPrinter.Formatter.mkAntiquot.formatter
(name : String)
(kind : Option Lean.SyntaxNodeKind)
(anonymous : optParam Bool true)
:
Equations
- Lean.PrettyPrinter.Formatter.mkAntiquot.formatter name kind anonymous = Lean.Parser.mkAntiquot.formatter name kind anonymous
Equations
- Lean.PrettyPrinter.Formatter.interpretParserDescr x = match x with | Lean.ParserDescr.const n => liftM (Lean.Parser.getConstAlias Lean.PrettyPrinter.Formatter.formatterAliasesRef n) | Lean.ParserDescr.unary n d => do let a ← liftM (Lean.Parser.getUnaryAlias Lean.PrettyPrinter.Formatter.formatterAliasesRef n) let a_1 ← Lean.PrettyPrinter.Formatter.interpretParserDescr d pure (a a_1) | Lean.ParserDescr.binary n d₁ d₂ => do let a ← liftM (Lean.Parser.getBinaryAlias Lean.PrettyPrinter.Formatter.formatterAliasesRef n) let a_1 ← Lean.PrettyPrinter.Formatter.interpretParserDescr d₁ let a_2 ← Lean.PrettyPrinter.Formatter.interpretParserDescr d₂ pure (a a_1 a_2) | Lean.ParserDescr.node k prec d => do let a ← Lean.PrettyPrinter.Formatter.interpretParserDescr d pure (Lean.PrettyPrinter.Formatter.node.formatter k a) | Lean.ParserDescr.nodeWithAntiquot x k d => do let a ← Lean.PrettyPrinter.Formatter.interpretParserDescr d pure (Lean.PrettyPrinter.Formatter.node.formatter k a) | Lean.ParserDescr.sepBy p sep psep trail => do let a ← Lean.PrettyPrinter.Formatter.interpretParserDescr p let a_1 ← Lean.PrettyPrinter.Formatter.interpretParserDescr psep pure (Lean.Parser.sepBy.formatter a sep a_1 trail) | Lean.ParserDescr.sepBy1 p sep psep trail => do let a ← Lean.PrettyPrinter.Formatter.interpretParserDescr p let a_1 ← Lean.PrettyPrinter.Formatter.interpretParserDescr psep pure (Lean.Parser.sepBy1.formatter a sep a_1 trail) | Lean.ParserDescr.trailingNode k prec lhsPrec d => do let a ← Lean.PrettyPrinter.Formatter.interpretParserDescr d pure (Lean.PrettyPrinter.Formatter.trailingNode.formatter k prec lhsPrec a) | Lean.ParserDescr.symbol tk => pure (Lean.Parser.symbol.formatter tk) | Lean.ParserDescr.nonReservedSymbol tk includeIdent => pure (Lean.Parser.nonReservedSymbol.formatter tk false) | Lean.ParserDescr.parser constName => Lean.ParserCompiler.CombinatorAttribute.runDeclFor Lean.PrettyPrinter.combinatorFormatterAttribute constName | Lean.ParserDescr.cat catName prec => pure (Lean.PrettyPrinter.Formatter.categoryParser.formatter catName)