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

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

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

instance Lean.Syntax.instToFormat : Lean.ToFormat Lean.Syntax

Equations

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

instance Lean.Syntax.instToString : ToString Lean.Syntax

Equations

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

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

Equations

• Lean.Syntax.instToFormatTSyntax = { format := fun (x : Lean.TSyntax k) => Lean.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 }