instance Lean.IR.instToFormatArg : Lean.ToFormat Lean.IR.Arg

Equations

• Lean.IR.instToFormatArg = { format := Lean.IR.formatArg }

def Lean.IR.formatArray {α : Type} [Lean.ToFormat α] (args : Array α) : Lean.Format

Equations

• Lean.IR.formatArray args = Array.foldl (fun (r : Lean.Format) (a : α) => r ++ Std.Format.text " " ++ Std.format a) Lean.Format.nil args 0

instance Lean.IR.instToFormatLitVal : Lean.ToFormat Lean.IR.LitVal

Equations

• Lean.IR.instToFormatLitVal = { format := Lean.IR.formatLitVal }

instance Lean.IR.instToFormatCtorInfo : Lean.ToFormat Lean.IR.CtorInfo

Equations

• Lean.IR.instToFormatCtorInfo = { format := Lean.IR.formatCtorInfo }

instance Lean.IR.instToFormatExpr : Lean.ToFormat Lean.IR.Expr

Equations

• Lean.IR.instToFormatExpr = { format := Lean.IR.formatExpr }

instance Lean.IR.instToStringExpr : ToString Lean.IR.Expr

Equations

• Lean.IR.instToStringExpr = { toString := fun (e : Lean.IR.Expr) => Lean.Format.pretty (Std.format e) Std.Format.defWidth 0 }

instance Lean.IR.instToFormatIRType : Lean.ToFormat Lean.IR.IRType

Equations

• Lean.IR.instToFormatIRType = { format := Lean.IR.formatIRType }

instance Lean.IR.instToStringIRType : ToString Lean.IR.IRType

Equations

• Lean.IR.instToStringIRType = { toString := toString ∘ Std.format }

instance Lean.IR.instToFormatParam : Lean.ToFormat Lean.IR.Param

Equations

• Lean.IR.instToFormatParam = { format := Lean.IR.formatParam }

def Lean.IR.formatAlt (fmt : Lean.IR.FnBody → Lean.Format) (indent : Nat) : Lean.IR.Alt → Lean.Format

Equations

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

def Lean.IR.formatParams (ps : Array Lean.IR.Param) : Lean.Format

Equations

• Lean.IR.formatParams ps = Lean.IR.formatArray ps

def Lean.IR.formatFnBodyHead : Lean.IR.FnBody → Lean.Format

Equations

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

def Lean.IR.formatFnBody (fnBody : Lean.IR.FnBody) (indent : optParam Nat 2) : Lean.Format

Equations

• Lean.IR.formatFnBody fnBody indent = Lean.IR.formatFnBody.loop indent fnBody

partial def Lean.IR.formatFnBody.loop (indent : optParam Nat 2) : Lean.IR.FnBody → Lean.Format

instance Lean.IR.instToFormatFnBody : Lean.ToFormat Lean.IR.FnBody

Equations

• Lean.IR.instToFormatFnBody = { format := fun (fnBody : Lean.IR.FnBody) => Lean.IR.formatFnBody fnBody }

instance Lean.IR.instToStringFnBody : ToString Lean.IR.FnBody

Equations

• Lean.IR.instToStringFnBody = { toString := fun (b : Lean.IR.FnBody) => Lean.Format.pretty (Std.format b) Std.Format.defWidth 0 }

def Lean.IR.formatDecl (decl : Lean.IR.Decl) (indent : optParam Nat 2) : Lean.Format

Equations

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

instance Lean.IR.instToFormatDecl : Lean.ToFormat Lean.IR.Decl

Equations

• Lean.IR.instToFormatDecl = { format := fun (decl : Lean.IR.Decl) => Lean.IR.formatDecl decl }

@[export lean_ir_decl_to_string]

def Lean.IR.declToString (d : Lean.IR.Decl) : String

Equations

• Lean.IR.declToString d = Lean.Format.pretty (Std.format d) Std.Format.defWidth 0

instance Lean.IR.instToStringDecl : ToString Lean.IR.Decl

Equations

• Lean.IR.instToStringDecl = { toString := Lean.IR.declToString }