def Lean.IR.irTypeForEnum (numCtors : Nat) : IRType

opaque Lean.IR.irTypeExt : Compiler.LCNF.CacheExtension Name IRType

opaque Lean.IR.trivialStructureInfoExt : Compiler.LCNF.CacheExtension Name (Option Compiler.LCNF.TrivialStructureInfo)

def Lean.IR.hasTrivialStructure? (declName : Name) : CoreM (Option Compiler.LCNF.TrivialStructureInfo)

The idea of this function is the same as in ToMono, however the notion of "irrelevancy" has changed because we now have the void type which can only be erased in impure context and thus at earliest at the conversion from mono to IR.

def Lean.IR.nameToIRType (name : Name) : CoreM IRType

partial def Lean.IR.toIRType (type : Lean.Expr) : CoreM IRType

inductive Lean.IR.CtorFieldInfo : Type

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

instance Lean.IR.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

def Lean.IR.instInhabitedCtorFieldInfo.default : CtorFieldInfo

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

instance Lean.IR.CtorFieldInfo.instToFormat : ToFormat CtorFieldInfo

structure Lean.IR.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

def Lean.IR.instInhabitedCtorLayout.default : CtorLayout

instance Lean.IR.instInhabitedCtorLayout : Inhabited CtorLayout

opaque Lean.IR.ctorLayoutExt : Compiler.LCNF.CacheExtension Name CtorLayout

def Lean.IR.getCtorLayout (ctorName : Name) : CoreM CtorLayout