partial def Lean.Syntax.formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Lean.Syntax → Lean.Format

def Lean.Syntax.formatStx (stx : Lean.Syntax) (maxDepth : optParam (Option Nat) none) (showInfo : optParam Bool false) : Lean.Format

Pretty print the given syntax stx as a Format. Nodes deeper than maxDepth are omitted. Setting the showInfo flag will also print the SourceInfo for each node.

Equations

• Lean.Syntax.formatStx stx maxDepth showInfo = Lean.Syntax.formatStxAux maxDepth showInfo 0 stx

instance Lean.Syntax.instToFormatSyntax : Lean.ToFormat Lean.Syntax

Equations

• Lean.Syntax.instToFormatSyntax = { format := fun (stx : Lean.Syntax) => Lean.Syntax.formatStx stx none }

instance Lean.Syntax.instToStringSyntax : ToString Lean.Syntax

Equations

• Lean.Syntax.instToStringSyntax = { toString := toString ∘ Std.format }

instance Lean.Syntax.instToFormatTSyntax {k : Lean.SyntaxNodeKinds} : Lean.ToFormat (Lean.TSyntax k)

Equations

• Lean.Syntax.instToFormatTSyntax = { format := fun (x : Lean.TSyntax k) => Std.format x.raw }

instance Lean.Syntax.instToStringTSyntax {k : Lean.SyntaxNodeKinds} : ToString (Lean.TSyntax k)

Equations

• Lean.Syntax.instToStringTSyntax = { toString := fun (x : Lean.TSyntax k) => toString x.raw }