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

def Lean.Syntax.formatStx (stx : Syntax) (maxDepth : Option Nat := none) (showInfo : Bool := false) : Std.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

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

instance Lean.Syntax.instToFormat : Std.ToFormat Syntax

Equations

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

instance Lean.Syntax.instToString : ToString Syntax

Equations

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

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

Equations

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

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

Equations

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