← Copula mathematical handbook

def Lean.IR.nameToIRType (n : Name) : IRType

Equations

• Lean.IR.nameToIRType `Float = Lean.IR.IRType.float
• Lean.IR.nameToIRType `Float32 = Lean.IR.IRType.float32
• Lean.IR.nameToIRType `UInt8 = Lean.IR.IRType.uint8
• Lean.IR.nameToIRType `UInt16 = Lean.IR.IRType.uint16
• Lean.IR.nameToIRType `UInt32 = Lean.IR.IRType.uint32
• Lean.IR.nameToIRType `UInt64 = Lean.IR.IRType.uint64
• Lean.IR.nameToIRType `lcErased = Lean.IR.IRType.erased
• Lean.IR.nameToIRType `obj = Lean.IR.IRType.object
• Lean.IR.nameToIRType `tobj = Lean.IR.IRType.tobject
• Lean.IR.nameToIRType `tagged = Lean.IR.IRType.tagged
• Lean.IR.nameToIRType `lcVoid = Lean.IR.IRType.void
• Lean.IR.nameToIRType n = panicWithPosWithDecl "Lean.Compiler.IR.ToIRType" "Lean.IR.nameToIRType" 32 9 "unreachable code has been reached"

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

Equations

• Lean.IR.toIRType (Lean.Expr.const `Float []) = Lean.IR.IRType.float
• Lean.IR.toIRType (Lean.Expr.const `Float32 []) = Lean.IR.IRType.float32
• Lean.IR.toIRType (Lean.Expr.const `UInt8 []) = Lean.IR.IRType.uint8
• Lean.IR.toIRType (Lean.Expr.const `UInt16 []) = Lean.IR.IRType.uint16
• Lean.IR.toIRType (Lean.Expr.const `UInt32 []) = Lean.IR.IRType.uint32
• Lean.IR.toIRType (Lean.Expr.const `UInt64 []) = Lean.IR.IRType.uint64
• Lean.IR.toIRType (Lean.Expr.const `USize []) = Lean.IR.IRType.usize
• Lean.IR.toIRType (Lean.Expr.const `lcErased []) = Lean.IR.IRType.erased
• Lean.IR.toIRType (Lean.Expr.const `obj []) = Lean.IR.IRType.object
• Lean.IR.toIRType (Lean.Expr.const `tobj []) = Lean.IR.IRType.tobject
• Lean.IR.toIRType (Lean.Expr.const `tagged []) = Lean.IR.IRType.tagged
• Lean.IR.toIRType (Lean.Expr.const `lcVoid []) = Lean.IR.IRType.void
• Lean.IR.toIRType type = panicWithPosWithDecl "Lean.Compiler.IR.ToIRType" "Lean.IR.toIRType" 49 9 "unreachable code has been reached"