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

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

Instances For

source
opaque Lean.IR.irTypeExt :
Compiler.LCNF.CacheExtension Name IRType
source
def Lean.IR.nameToIRType (name : Name) :
CoreM IRType
Equations

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

Instances For

source
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 b binderInfo) = if Lean.IR.isAnyProducingType✝ b = true then pure Lean.IR.IRType.tobject else 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" 103 9 "unreachable code has been reached"

Instances For

source
inductive Lean.IR.CtorFieldInfo :
Type

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

Instances For

source
instance Lean.IR.instInhabitedCtorFieldInfo :
Inhabited CtorFieldInfo
Equations

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

source
def Lean.IR.instInhabitedCtorFieldInfo.default :
CtorFieldInfo
Equations

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

Instances For

source
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
- (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

Instances For

source
instance Lean.IR.CtorFieldInfo.instToFormat :
ToFormat CtorFieldInfo
Equations

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

source
structure Lean.IR.CtorLayout :
Type

- ctorInfo : CtorInfo
- fieldInfo : Array CtorFieldInfo

Instances For

source
instance Lean.IR.instInhabitedCtorLayout :
Inhabited CtorLayout
Equations

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

source
def Lean.IR.instInhabitedCtorLayout.default :
CtorLayout
Equations

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

Instances For

source
opaque Lean.IR.ctorLayoutExt :
Compiler.LCNF.CacheExtension Name CtorLayout
source
def Lean.IR.getCtorLayout (ctorName : Name) :
CoreM CtorLayout
Equations

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

Instances For