inductive Lean.IR.CtorFieldInfo : Type

• irrelevant : CtorFieldInfo
• object (i : Nat) : CtorFieldInfo
• usize (i : Nat) : CtorFieldInfo
• scalar (sz offset : Nat) (type : IRType) : CtorFieldInfo

instance Lean.IR.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

def Lean.IR.CtorFieldInfo.format : CtorFieldInfo → Format

instance Lean.IR.CtorFieldInfo.instToFormat : ToFormat CtorFieldInfo

structure Lean.IR.CtorLayout : Type

• cidx : Nat
• fieldInfo : List CtorFieldInfo
• numObjs : Nat
• numUSize : Nat
• scalarSize : Nat

@[extern lean_ir_get_ctor_layout]

opaque Lean.IR.getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout