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 }

instance Lean.Syntax.instToFormatTSyntax {k : Lean.SyntaxNodeKinds} :

Lean.ToFormat (Lean.TSyntax k)

Equations

Lean.Syntax.instToFormatTSyntax = { format := fun a => Lean.format a.raw }

instance Lean.Syntax.instToStringTSyntax {k : Lean.SyntaxNodeKinds} :

ToString (Lean.TSyntax k)

Equations

Lean.Syntax.instToStringTSyntax = { toString := fun a => toString a.raw }