Documentation

Init.Data.Format.Syntax

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

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
Instances For
    Equations
    • Lean.Syntax.instToFormatTSyntax = { format := fun x => Std.format x.raw }
    Equations
    • Lean.Syntax.instToStringTSyntax = { toString := fun x => toString x.raw }