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

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

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]

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