Documentation

Init.Data.Format.Syntax

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) :

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.formatStx stx none }

instance Lean.Syntax.instToStringSyntax :

ToString Lean.Syntax

Equations

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