Documentation

Lean.Compiler.IR.Format

instance Lean.IR.instToFormatArg:

Lean.ToFormat Lean.IR.Arg

Equations

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

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

Equations

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

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.Format.pretty (Lean.format e) }

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 ∘ Lean.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) :

Equations

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

@[export lean_ir_format_fn_body_head]

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

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.formatFnBody fnBody }

instance Lean.IR.instToStringFnBody:

ToString Lean.IR.FnBody

Equations

Lean.IR.instToStringFnBody = { toString := fun b => Lean.Format.pretty (Lean.format b) }

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

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.formatDecl decl }

@[export lean_ir_decl_to_string]

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

Equations

Lean.IR.declToString d = Lean.Format.pretty (Lean.format d)

instance Lean.IR.instToStringDecl:

ToString Lean.IR.Decl

Equations

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