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

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

Equations

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

def Lean.IR.toIRType (type : Lean.Expr) : CoreM IRType

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.toIRType (Lean.Expr.const name us) = Lean.IR.nameToIRType name
• Lean.IR.toIRType (Lean.Expr.forallE binderName binderType body binderInfo) = pure Lean.IR.IRType.object
• Lean.IR.toIRType (Lean.Expr.mdata data b) = Lean.IR.toIRType b
• Lean.IR.toIRType type = panicWithPosWithDecl "Lean.Compiler.IR.ToIRType" "Lean.IR.toIRType" 91 9 "unreachable code has been reached"

inductive Lean.IR.CtorFieldInfo : Type

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

instance Lean.IR.instInhabitedCtorFieldInfo : Inhabited 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.object i type).format = Std.format "obj@" ++ Std.format i ++ Std.format ":" ++ Std.format type ++ Std.format ""
• (Lean.IR.CtorFieldInfo.usize i).format = Std.format "usize@" ++ Std.format i ++ Std.format ""
• (Lean.IR.CtorFieldInfo.scalar sz offset type).format = Std.format "scalar#" ++ Std.format sz ++ Std.format "@" ++ Std.format offset ++ Std.format ":" ++ Std.format type ++ Std.format ""

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

instance Lean.IR.instInhabitedCtorLayout : Inhabited CtorLayout

Equations

• Lean.IR.instInhabitedCtorLayout = { default := { ctorInfo := default, fieldInfo := 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.