Documentation

Lean.PrettyPrinter.Parenthesizer

Equations
  • Lean.PrettyPrinter.instOrElseParenthesizerM = { orElse := Lean.PrettyPrinter.ParenthesizerM.orElse }
Equations
Equations
Equations
  • Lean.PrettyPrinter.mkCombinatorParenthesizerAttribute = Lean.ParserCompiler.registerCombinatorAttribute `combinatorParenthesizer "Register a parenthesizer for a parser combinator.\n\n [combinatorParenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`.\n Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds.\n The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced\n with `Parenthesizer` in the parameter types."
Equations
Equations
Equations
Equations
Equations
@[extern lean_pretty_printer_parenthesizer_interpret_parser_descr]
@[implementedBy Lean.PrettyPrinter.Parenthesizer.parenthesizerForKindUnsafe]
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations