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

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

Except String Lean.IR.CtorLayout