def Lean.Compiler.LCNF.setHasTrivialImpureStructure? (declName : Name) : CoreM Unit

Eagerly computes and persists the impure trivial-structure info of declName; see compileDecls.

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

def Lean.Compiler.LCNF.setImpureType (name : Name) : CoreM Unit

Eagerly computes and persists the IR type of inductive name; see compileDecls.

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

Returns the IR (impure) type representation of name. Requires compileDecls to have been run for inductive type name.

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

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

def Lean.Compiler.LCNF.setCtorLayout (ctorName : Name) : CoreM Unit

Eagerly computes and persists the layout of constructor ctorName; see compileDecls.

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

Returns the runtime layout of constructor ctorName. Requires compileDecls to have been run for its inductive type.

def Lean.Compiler.LCNF.compileInductives (typeNames : Array Name) : CoreM Unit

Eagerly computes and persists all cross-module compiler caches for the inductive types typeNames (and their constructors) in their defining module; run from compileDecls.