The formatter turns a Syntax tree into a Format object, inserting both mandatory whitespace (to separate adjacent tokens) as well as "pretty" optional whitespace.

The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree, driven by parser-specific handlers registered via attributes. The traversal is right-to-left so that when emitting a token, we already know the text following it and can decide whether or not whitespace between the two is necessary.

structure Lean.PrettyPrinter.Formatter.Context : Type

• options : Lean.Options
• table : Lean.Parser.TokenTable

structure Lean.PrettyPrinter.Formatter.State : Type

• stxTrav : Lean.Syntax.Traverser
• leadWord : String
• isUngrouped : Bool
• mustBeGrouped : Bool
• stack : Array Lean.Format

@[reducible, inline]

abbrev Lean.PrettyPrinter.FormatterM (α : Type) : Type

Equations

• Lean.PrettyPrinter.FormatterM = ReaderT Lean.PrettyPrinter.Formatter.Context (StateRefT' IO.RealWorld Lean.PrettyPrinter.Formatter.State Lean.CoreM)

@[inline]

def Lean.PrettyPrinter.FormatterM.orElse {α : Type} (p₁ : Lean.PrettyPrinter.FormatterM α) (p₂ : Unit → Lean.PrettyPrinter.FormatterM α) : Lean.PrettyPrinter.FormatterM α

Equations

• p₁.orElse p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun (x : Lean.Exception) => do set s p₂ ()

instance Lean.PrettyPrinter.instOrElseFormatterM {α : Type} : OrElse (Lean.PrettyPrinter.FormatterM α)

Equations

• Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter : Type

Equations

• Lean.PrettyPrinter.Formatter = Lean.PrettyPrinter.FormatterM Unit

unsafe def Lean.PrettyPrinter.mkFormatterAttribute : IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter)

opaque Lean.PrettyPrinter.formatterAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter

unsafe def Lean.PrettyPrinter.mkCombinatorFormatterAttribute : IO Lean.ParserCompiler.CombinatorAttribute

opaque Lean.PrettyPrinter.combinatorFormatterAttribute : Lean.ParserCompiler.CombinatorAttribute

def Lean.PrettyPrinter.Formatter.throwBacktrack {α : Type} : Lean.PrettyPrinter.FormatterM α

Equations

• Lean.PrettyPrinter.Formatter.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)

instance Lean.PrettyPrinter.Formatter.instMonadTraverserFormatterM : Lean.Syntax.MonadTraverser Lean.PrettyPrinter.FormatterM

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.getStack : Lean.PrettyPrinter.FormatterM (Array Lean.Format)

Equations

• Lean.PrettyPrinter.Formatter.getStack = do let st ← get pure st.stack

def Lean.PrettyPrinter.Formatter.getStackSize : Lean.PrettyPrinter.FormatterM Nat

Equations

• Lean.PrettyPrinter.Formatter.getStackSize = do let stack ← Lean.PrettyPrinter.Formatter.getStack pure stack.size

def Lean.PrettyPrinter.Formatter.setStack (stack : Array Lean.Format) : Lean.PrettyPrinter.FormatterM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.pushWhitespace (f : Lean.Format) : Lean.PrettyPrinter.FormatterM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.pushLine : Lean.PrettyPrinter.FormatterM Unit

Equations

• Lean.PrettyPrinter.Formatter.pushLine = Lean.PrettyPrinter.Formatter.pushWhitespace Lean.Format.line

def Lean.PrettyPrinter.Formatter.pushAlign (force : Bool) : Lean.PrettyPrinter.FormatterM Unit

Equations

• Lean.PrettyPrinter.Formatter.pushAlign force = Lean.PrettyPrinter.Formatter.pushWhitespace (Lean.Format.align force)

def Lean.PrettyPrinter.Formatter.visitArgs (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.FormatterM Unit

Execute x at the right-most child of the current node, if any, then advance to the left. Runs x even if there are no children, in which case the current syntax node will be .missing.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.fold (fn : Array Lean.Format → Lean.Format) (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.FormatterM Unit

Execute x, pass array of generated Format objects to fn, and push result.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.concat (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.FormatterM Unit

Execute x and concatenate generated Format objects.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.indent (x : Lean.PrettyPrinter.Formatter) (indent : optParam (Option Int) none) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.fill (x : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.group (x : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.withMaybeTag (pos? : Option String.Pos) (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.Formatter

If pos? has a position, run x and tag its results with that position, if they are not already tagged. Otherwise just run x.

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Formatter.withMaybeTag pos? x = x

partial def Lean.PrettyPrinter.Formatter.orelse.formatter (p1 : Lean.PrettyPrinter.Formatter) (p2 : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

def Lean.PrettyPrinter.Formatter.recover.formatter (fmt : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.recover.formatter fmt = fmt

def Lean.PrettyPrinter.Formatter.recover'.formatter (fmt : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.recover'.formatter fmt = fmt

@[extern lean_mk_antiquot_formatter]

opaque Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : optParam Bool true) (isPseudoKind : optParam Bool false) : Lean.PrettyPrinter.Formatter

@[extern lean_pretty_printer_formatter_interpret_parser_descr]

opaque Lean.PrettyPrinter.Formatter.interpretParserDescr' : Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Formatter

unsafe def Lean.PrettyPrinter.Formatter.formatterForKindUnsafe (k : Lean.SyntaxNodeKind) : Lean.PrettyPrinter.Formatter

@[implemented_by Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]

opaque Lean.PrettyPrinter.Formatter.formatterForKind (k : Lean.SyntaxNodeKind) : Lean.PrettyPrinter.Formatter

def Lean.PrettyPrinter.Formatter.withAntiquot.formatter (antiP : Lean.PrettyPrinter.Formatter) (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.withAntiquot.formatter antiP p = Lean.PrettyPrinter.Formatter.orelse.formatter antiP p

def Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.tokenWithAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.categoryFormatterCore (cat : Lake.Name) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.categoryParser.formatter (cat : Lake.Name) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.categoryFormatter (cat : Lake.Name) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.categoryFormatter cat = (Lean.PrettyPrinter.Formatter.categoryFormatterCore cat).indent.fill

def Lean.PrettyPrinter.Formatter.parserOfStack.formatter (offset : Nat) (_prec : optParam Nat 0) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.error.formatter (_msg : String) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.error.formatter _msg = pure ()

def Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter _msg _delta = pure ()

def Lean.PrettyPrinter.Formatter.lookahead.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.lookahead.formatter x = pure ()

def Lean.PrettyPrinter.Formatter.notFollowedBy.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.notFollowedBy.formatter x = pure ()

def Lean.PrettyPrinter.Formatter.andthen.formatter (p1 : Lean.PrettyPrinter.Formatter) (p2 : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = SeqRight.seqRight p2 fun (x : Unit) => p1

def Lean.PrettyPrinter.Formatter.checkKind (k : Lean.SyntaxNodeKind) : Lean.PrettyPrinter.FormatterM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.node.formatter (k : Lean.SyntaxNodeKind) (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.node.formatter k p = do Lean.PrettyPrinter.Formatter.checkKind k Lean.PrettyPrinter.Formatter.visitArgs p

def Lean.PrettyPrinter.Formatter.withFn.formatter : (Lean.Parser.ParserFn → Lean.Parser.ParserFn) → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.withFn.formatter x p = p

def Lean.PrettyPrinter.Formatter.trailingNode.formatter (k : Lean.SyntaxNodeKind) : Nat → Nat → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.parseToken (s : String) : Lean.PrettyPrinter.FormatterM Lean.Parser.ParserState

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.pushToken (info : Lean.SourceInfo) (tk : String) : Lean.PrettyPrinter.FormatterM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter (sym : String) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter (sym : String) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.rawCh.formatter (ch : Char) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.rawCh.formatter ch = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter ch.toString

def Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter (sym : String) (asciiSym : String) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.identEq.formatter (_id : Lake.Name) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.identEq.formatter _id = Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.visitAtom (k : Lean.SyntaxNodeKind) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.charLitKind

def Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.strLitKind

def Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.nameLitKind

def Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.numLitKind

def Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.scientificLitKind

def Lean.PrettyPrinter.Formatter.fieldIdx.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.fieldIdx.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.fieldIdxKind

def Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.visitArgs (stx.getArgs.size.forM fun (x : Nat) => p)

def Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter p = Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p

def Lean.PrettyPrinter.Formatter.optionalNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.many1Unbox.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) (pSep : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter (p : Lean.PrettyPrinter.Formatter) (pSep : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter = Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.withoutInfo.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.withoutInfo.formatter p = p

def Lean.PrettyPrinter.Formatter.checkWsBefore.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkWsBefore.formatter = do let st ← get if (st.leadWord != "") = true then Lean.PrettyPrinter.Formatter.pushLine else pure PUnit.unit

def Lean.PrettyPrinter.Formatter.checkPrec.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.setLhsPrec.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.setLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkStackTop.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkStackTop.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkTailWs.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkTailWs.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColEq.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColEq.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGe.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColGe.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGt.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColGt.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLineEq.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLineEq.formatter = pure ()

def Lean.PrettyPrinter.Formatter.eoi.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.eoi.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter = pure ()

def Lean.PrettyPrinter.Formatter.skip.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.skip.formatter = pure ()

def Lean.PrettyPrinter.Formatter.pushNone.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.pushNone.formatter = Lean.Syntax.MonadTraverser.goLeft

def Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter = Lean.Syntax.MonadTraverser.goLeft

def Lean.PrettyPrinter.Formatter.interpolatedStr.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

• One or more equations did not get rendered due to their size.

@[macro_inline]

def Lean.PrettyPrinter.Formatter.ite : {x : Type} → (c : Prop) → [inst : Decidable c] → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

Equations

• Lean.PrettyPrinter.Formatter.ite c t e = if c then t else e

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type

Equations

• Lean.PrettyPrinter.Formatter.FormatterAliasValue = Lean.Parser.AliasValue Lean.PrettyPrinter.Formatter

opaque Lean.PrettyPrinter.Formatter.formatterAliasesRef : IO.Ref (Lake.NameMap Lean.PrettyPrinter.Formatter.FormatterAliasValue)

def Lean.PrettyPrinter.Formatter.registerAlias (aliasName : Lake.Name) (v : Lean.PrettyPrinter.Formatter.FormatterAliasValue) : IO Unit

Equations

• Lean.PrettyPrinter.Formatter.registerAlias aliasName v = Lean.Parser.registerAliasCore Lean.PrettyPrinter.Formatter.formatterAliasesRef aliasName v

instance Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue : Coe Lean.PrettyPrinter.Formatter Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue = { coe := Lean.Parser.AliasValue.const }

instance Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue : Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter) Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.unary }

instance Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue : Coe (Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter) Lean.PrettyPrinter.Formatter.FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.binary }

opaque Lean.PrettyPrinter.pp.oneline : Lean.Option Bool

def Lean.PrettyPrinter.format (formatter : Lean.PrettyPrinter.Formatter) (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

• One or more equations did not get rendered due to their size.

def Lean.PrettyPrinter.formatCategory (cat : Lake.Name) (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.formatCategory cat = Lean.PrettyPrinter.format (Lean.PrettyPrinter.Formatter.categoryFormatter cat)

def Lean.PrettyPrinter.formatTerm (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.formatTerm = Lean.PrettyPrinter.formatCategory `term

def Lean.PrettyPrinter.formatTactic (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.formatTactic = Lean.PrettyPrinter.formatCategory `tactic

def Lean.PrettyPrinter.formatCommand (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.formatCommand = Lean.PrettyPrinter.formatCategory `command