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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

• Lean.IR.instInhabitedCtorFieldInfo = { default := Lean.IR.instInhabitedCtorFieldInfo.default }

def Lean.IR.instInhabitedCtorFieldInfo.default : CtorFieldInfo

Equations

• Lean.IR.instInhabitedCtorFieldInfo.default = Lean.IR.CtorFieldInfo.erased

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

Equations

• Lean.IR.CtorFieldInfo.erased.format = Std.Format.text "◾"
• Lean.IR.CtorFieldInfo.void.format = Std.Format.text "void"
• (Lean.IR.CtorFieldInfo.object i type).format = Std.format "obj@" ++ Std.format i ++ Std.format ":" ++ Std.format type
• (Lean.IR.CtorFieldInfo.usize i).format = Std.format "usize@" ++ Std.format i
• (Lean.IR.CtorFieldInfo.scalar sz offset type).format = Std.format "scalar#" ++ Std.format sz ++ Std.format "@" ++ Std.format offset ++ Std.format ":" ++ Std.format type

instance Lean.IR.CtorFieldInfo.instToFormat : ToFormat CtorFieldInfo

Equations

• Lean.IR.CtorFieldInfo.instToFormat = { format := Lean.IR.CtorFieldInfo.format }

structure Lean.IR.CtorLayout : Type

• ctorInfo : CtorInfo
• fieldInfo : Array CtorFieldInfo

def Lean.IR.instInhabitedCtorLayout.default : CtorLayout

Equations

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

instance Lean.IR.instInhabitedCtorLayout : Inhabited CtorLayout

Equations

• Lean.IR.instInhabitedCtorLayout = { default := Lean.IR.instInhabitedCtorLayout.default }

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

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

Equations

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