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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.hasTrivialImpureStructure? declName = Lean.Compiler.LCNF.Irrelevant.hasTrivialStructure? Lean.Compiler.LCNF.impureTrivialStructureInfoExt✝ declName

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

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

Equations

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

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.

Equations

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedCtorFieldInfo = { default := Lean.Compiler.LCNF.instInhabitedCtorFieldInfo.default }

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

Equations

• Lean.Compiler.LCNF.instInhabitedCtorLayout = { default := Lean.Compiler.LCNF.instInhabitedCtorLayout.default }

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

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

Equations

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

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.

Equations

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

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.

Equations

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