opaque Lean.IR.scalarTypeExt : Compiler.LCNF.CacheExtension Name (Option IRType)

def Lean.IR.lowerEnumToScalarType? (name : Name) : CoreM (Option IRType)

Equations

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

def Lean.IR.lowerEnumToScalarType?.fillCache (name : Name) : CoreM (Option IRType)

Equations

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

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

inductive Lean.IR.CtorFieldInfo : Type

• irrelevant : CtorFieldInfo
• object (i : Nat) : 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.irrelevant }

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

Equations

• Lean.IR.CtorFieldInfo.irrelevant.format = Std.Format.text "◾"
• (Lean.IR.CtorFieldInfo.object i).format = Std.format "obj@" ++ Std.format i ++ 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

• cidx : Nat
• fieldInfo : List CtorFieldInfo
• numObjs : Nat
• numUSize : Nat
• scalarSize : Nat

@[extern lean_ir_get_ctor_layout]

opaque Lean.IR.getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout

opaque Lean.IR.ctorInfoExt : Compiler.LCNF.CacheExtension Name (CtorInfo × Array CtorFieldInfo)

def Lean.IR.getCtorInfo (name : Name) : CoreM (CtorInfo × Array CtorFieldInfo)

Equations

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

def Lean.IR.getCtorInfo.fillCache (name : Name) : CoreM (CtorInfo × Array CtorFieldInfo)

Equations

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