Pretty-printing for SurfaceTLAPlus, used by -d-style AST dumps.

partial def SurfaceTLAPlus.Typ.pretty : Typ → Std.Format

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatTyp : Std.ToFormat Typ

Equations

• SurfaceTLAPlus.instToFormatTyp = { format := SurfaceTLAPlus.Typ.pretty }

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatPrefixOperator : Std.ToFormat PrefixOperator

Equations

• SurfaceTLAPlus.instToFormatPrefixOperator = { format := Std.Format.text ∘ toString }

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatInfixOperator : Std.ToFormat InfixOperator

Equations

• SurfaceTLAPlus.instToFormatInfixOperator = { format := Std.Format.text ∘ toString }

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatPostfixOperator : Std.ToFormat PostfixOperator

Equations

• SurfaceTLAPlus.instToFormatPostfixOperator = { format := Std.Format.text ∘ toString }

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatIdentifierOrTuple {α : Type} [Std.ToFormat α] : Std.ToFormat (IdentifierOrTuple α)

Equations

• One or more equations did not get rendered due to their size.

def SurfaceTLAPlus.QuantifierBound.pretty {α β : Type} [Std.ToFormat α] (f : β → Std.Format) : QuantifierBound α β → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• SurfaceTLAPlus.QuantifierBound.pretty f (SurfaceTLAPlus.QuantifierBound.var ann x_1 e) = Std.format ann ++ (Std.format " " ++ Std.format x_1 ++ Std.format " \\in ") ++ f e

partial def SurfaceTLAPlus.Expression.pretty {α : Type} [Std.ToFormat α] (e : Expression α) : Std.Format

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatExpression {α : Type} [Std.ToFormat α] : Std.ToFormat (Expression α)

Equations

• SurfaceTLAPlus.instToFormatExpression = { format := SurfaceTLAPlus.Expression.pretty }

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatDeclaration {α : Type} [Std.ToFormat α] : Std.ToFormat (Declaration α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance SurfaceTLAPlus.instToFormatModule {α β : Type} [Std.ToFormat α] [Std.ToFormat β] : Std.ToFormat (Module α β)

Equations

• One or more equations did not get rendered due to their size.