def Lean.Compiler.LCNF.hasTrivialImpureStructure? (declName : Name) : CoreM (Option 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 impure.

def Lean.Compiler.LCNF.nameToImpureType (name : Name) : CoreM Expr

partial def Lean.Compiler.LCNF.toImpureType (type : Expr) : CoreM Expr

inductive Lean.Compiler.LCNF.CtorFieldInfo : Type

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

def Lean.Compiler.LCNF.instInhabitedCtorFieldInfo.default : CtorFieldInfo

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

def Lean.Compiler.LCNF.instInhabitedCtorLayout.default : CtorLayout

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

def Lean.Compiler.LCNF.getCtorLayout (ctorName : Name) : CoreM CtorLayout

def Lean.Compiler.LCNF.getOtherDeclImpureType (declName : Name) : CoreM Expr