Documentation

Lean.PrettyPrinter.Formatter

Equations
  • Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }
Equations
Equations
  • Lean.PrettyPrinter.mkCombinatorFormatterAttribute = Lean.ParserCompiler.registerCombinatorAttribute `combinatorFormatter "Register a formatter for a parser combinator.\n\n [combinatorFormatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`.\n Note that, unlike with [formatter], 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 `Formatter` in the parameter types."
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
@[extern lean_mk_antiquot_formatter]
@[extern lean_pretty_printer_formatter_interpret_parser_descr]
@[implementedBy Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations