Documentation

Lean.Compiler.IR.CtorLayout

inductive Lean.IR.CtorFieldInfo :

Type

irrelevant: Lean.IR.CtorFieldInfo
object: Nat → Lean.IR.CtorFieldInfo
usize: Nat → Lean.IR.CtorFieldInfo
scalar: Nat → Nat → Lean.IR.IRType → Lean.IR.CtorFieldInfo

def Lean.IR.CtorFieldInfo.format :

Lean.IR.CtorFieldInfo → Lean.Format

Equations

Lean.IR.CtorFieldInfo.format x = match x with | Lean.IR.CtorFieldInfo.irrelevant => Std.Format.text "◾" | Lean.IR.CtorFieldInfo.object i => Lean.format "obj@" ++ Lean.format i ++ Lean.format "" | Lean.IR.CtorFieldInfo.usize i => Lean.format "usize@" ++ Lean.format i ++ Lean.format "" | Lean.IR.CtorFieldInfo.scalar sz offset type => Lean.format "scalar#" ++ Lean.format sz ++ Lean.format "@" ++ Lean.format offset ++ Lean.format ":" ++ Lean.format type ++ Lean.format ""

instance Lean.IR.CtorFieldInfo.instToFormatCtorFieldInfo :

Lean.ToFormat Lean.IR.CtorFieldInfo

Equations

Lean.IR.CtorFieldInfo.instToFormatCtorFieldInfo = { format := Lean.IR.CtorFieldInfo.format }

structure Lean.IR.CtorLayout :

Type

cidx : Nat
fieldInfo : List Lean.IR.CtorFieldInfo
numObjs : Nat
numUSize : Nat
scalarSize : Nat

@[extern lean_ir_get_ctor_layout]

constant Lean.IR.getCtorLayout (env : Lean.Environment) (ctorName : Lean.Name) :

Except String Lean.IR.CtorLayout