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.

Equations

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

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

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

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorFieldInfo : Inhabited CtorFieldInfo

Equations

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedCtorFieldInfo.default = Lean.Compiler.LCNF.CtorFieldInfo.erased

structure Lean.Compiler.LCNF.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

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

Equations

• Lean.Compiler.LCNF.instInhabitedCtorLayout.default = { ctorInfo := default, fieldInfo := default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorLayout : Inhabited CtorLayout

Equations

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

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

Equations

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

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

Equations

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