This file defines bindings for LLVM. The main mechanisms are to:

• Mirror the values of C enumerations.
• Create opaque values for LLVM's pointer based API
• Write bindings that are IO based, which mutate the underlying in-memory data structures to build IR.

structure Lean.LLVM.CodegenFileType : Type

• val : UInt64

def Lean.LLVM.CodegenFileType.AssemblyFile : CodegenFileType

Equations

• Lean.LLVM.CodegenFileType.AssemblyFile = { val := 0 }

def Lean.LLVM.CodegenFileType.ObjectFile : CodegenFileType

Equations

• Lean.LLVM.CodegenFileType.ObjectFile = { val := 1 }

structure Lean.LLVM.IntPredicate : Type

• val : UInt64

def Lean.LLVM.IntPredicate.EQ : IntPredicate

Equations

• Lean.LLVM.IntPredicate.EQ = { val := 32 }

def Lean.LLVM.IntPredicate.NE : IntPredicate

Equations

• Lean.LLVM.IntPredicate.NE = { val := Lean.LLVM.IntPredicate.EQ.val + 1 }

def Lean.LLVM.IntPredicate.UGT : IntPredicate

Equations

• Lean.LLVM.IntPredicate.UGT = { val := Lean.LLVM.IntPredicate.NE.val + 1 }

structure Lean.LLVM.AttributeIndex : Type

• val : UInt64

def Lean.LLVM.AttributeIndex.AttributeReturnIndex : AttributeIndex

Equations

• Lean.LLVM.AttributeIndex.AttributeReturnIndex = { val := 0 }

def Lean.LLVM.AttributeIndex.AttributeFunctionIndex : AttributeIndex

Equations

• Lean.LLVM.AttributeIndex.AttributeFunctionIndex = { val := 18446744073709551615 }

structure Lean.LLVM.BasicBlock {Context : Sort u_1} (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyBasicBlock {Context✝ : Sort u_1} {ctx : Context✝} : Nonempty (BasicBlock ctx)

structure Lean.LLVM.Builder {Context : Sort u_1} (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyBuilder {Context✝ : Sort u_1} {ctx : Context✝} : Nonempty (Builder ctx)

structure Lean.LLVM.Context : Type

• ptr : USize

instance Lean.LLVM.instNonemptyContext : Nonempty Context

structure Lean.LLVM.LLVMType (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyLLVMType {ctx : Context} : Nonempty (LLVMType ctx)

structure Lean.LLVM.MemoryBuffer (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyMemoryBuffer {ctx : Context} : Nonempty (MemoryBuffer ctx)

structure Lean.LLVM.Module (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyModule {ctx : Context} : Nonempty (Module ctx)

structure Lean.LLVM.Target (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyTarget {ctx : Context} : Nonempty (Target ctx)

structure Lean.LLVM.TargetMachine (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyTargetMachine {ctx : Context} : Nonempty (TargetMachine ctx)

structure Lean.LLVM.Value (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyValue {ctx : Context} : Nonempty (Value ctx)

def Lean.LLVM.Value.isNull {ctx : Context} (v : Value ctx) : Bool

Check if the value is a null pointer. -

Equations

• v.isNull = (v.ptr == 0)

@[extern lean_llvm_get_value_name2]

opaque Lean.LLVM.Value.getName {ctx : Context} (value : Value ctx) : BaseIO String

structure Lean.LLVM.Attribute (ctx : Context) : Type

• ptr : USize

instance Lean.LLVM.instNonemptyAttribute {ctx : Context} : Nonempty (Attribute ctx)

@[extern lean_llvm_initialize_target_info]

opaque Lean.LLVM.llvmInitializeTargetInfo : BaseIO Unit

@[extern lean_llvm_create_context]

opaque Lean.LLVM.createContext : BaseIO Context

@[extern lean_llvm_create_module]

opaque Lean.LLVM.createModule (ctx : Context) (name : String) : BaseIO (Module ctx)

@[extern lean_llvm_module_to_string]

opaque Lean.LLVM.moduleToString {ctx : Context} (m : Module ctx) : BaseIO String

@[extern lean_llvm_write_bitcode_to_file]

opaque Lean.LLVM.writeBitcodeToFile {ctx : Context} (m : Module ctx) (path : String) : BaseIO Unit

@[extern lean_llvm_add_function]

opaque Lean.LLVM.addFunction {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_first_function]

opaque Lean.LLVM.getFirstFunction {ctx : Context} (m : Module ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_next_function]

opaque Lean.LLVM.getNextFunction {ctx : Context} (glbl : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_named_function]

opaque Lean.LLVM.getNamedFunction {ctx : Context} (m : Module ctx) (name : String) : BaseIO (Option (Value ctx))

@[extern lean_llvm_add_global]

opaque Lean.LLVM.addGlobal {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_named_global]

opaque Lean.LLVM.getNamedGlobal {ctx : Context} (m : Module ctx) (name : String) : BaseIO (Option (Value ctx))

@[extern lean_llvm_get_first_global]

opaque Lean.LLVM.getFirstGlobal {ctx : Context} (m : Module ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_next_global]

opaque Lean.LLVM.getNextGlobal {ctx : Context} (glbl : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_global_string]

opaque Lean.LLVM.buildGlobalString {ctx : Context} (builder : Builder ctx) (value : String) (name : String := "") : BaseIO (Value ctx)

@[extern llvm_is_declaration]

opaque Lean.LLVM.isDeclaration {ctx : Context} (global : Value ctx) : BaseIO Bool

@[extern lean_llvm_set_initializer]

opaque Lean.LLVM.setInitializer {ctx : Context} (glbl val : Value ctx) : BaseIO Unit

@[extern lean_llvm_function_type]

opaque Lean.LLVM.functionType {ctx : Context} (retty : LLVMType ctx) (args : Array (LLVMType ctx)) (isVarArg : Bool := false) : BaseIO (LLVMType ctx)

@[extern lean_llvm_void_type_in_context]

opaque Lean.LLVM.voidType (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_int_type_in_context]

opaque Lean.LLVM.intTypeInContext (ctx : Context) (width : UInt64) : BaseIO (LLVMType ctx)

@[extern lean_llvm_opaque_pointer_type_in_context]

opaque Lean.LLVM.opaquePointerTypeInContext (ctx : Context) (addrspace : UInt64 := 0) : BaseIO (LLVMType ctx)

@[extern lean_llvm_float_type_in_context]

opaque Lean.LLVM.floatTypeInContext (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_double_type_in_context]

opaque Lean.LLVM.doubleTypeInContext (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_pointer_type]

opaque Lean.LLVM.pointerType {ctx : Context} (elemty : LLVMType ctx) : BaseIO (LLVMType ctx)

@[extern lean_llvm_array_type]

opaque Lean.LLVM.arrayType {ctx : Context} (elemty : LLVMType ctx) (nelem : UInt64) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_array]

opaque Lean.LLVM.constArray {ctx : Context} (elemty : LLVMType ctx) (vals : Array (Value ctx)) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_string]

opaque Lean.LLVM.constString (ctx : Context) (str : String) : BaseIO (Value ctx)

@[extern lean_llvm_const_pointer_null]

opaque Lean.LLVM.constPointerNull {ctx : Context} (elemty : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_undef]

opaque Lean.LLVM.getUndef {ctx : Context} (elemty : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_create_builder_in_context]

opaque Lean.LLVM.createBuilderInContext (ctx : Context) : BaseIO (Builder ctx)

@[extern lean_llvm_append_basic_block_in_context]

opaque Lean.LLVM.appendBasicBlockInContext (ctx : Context) (fn : Value ctx) (name : String) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_count_basic_blocks]

opaque Lean.LLVM.countBasicBlocks {ctx : Context} (fn : Value ctx) : BaseIO UInt64

@[extern lean_llvm_get_entry_basic_block]

opaque Lean.LLVM.getEntryBasicBlock {ctx : Context} (fn : Value ctx) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_get_first_instruction]

opaque Lean.LLVM.getFirstInstruction {ctx : Context} (bb : BasicBlock ctx) : BaseIO (Option (Value ctx))

@[extern lean_llvm_position_builder_before]

opaque Lean.LLVM.positionBuilderBefore {ctx : Context} (builder : Builder ctx) (instr : Value ctx) : BaseIO Unit

@[extern lean_llvm_position_builder_at_end]

opaque Lean.LLVM.positionBuilderAtEnd {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO Unit

@[extern lean_llvm_build_call2]

opaque Lean.LLVM.buildCall2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (fn : Value ctx) (args : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_set_tail_call]

opaque Lean.LLVM.setTailCall {ctx : Context} (fn : Value ctx) (istail : Bool) : BaseIO Unit

@[extern lean_llvm_build_cond_br]

opaque Lean.LLVM.buildCondBr {ctx : Context} (builder : Builder ctx) (if_ : Value ctx) (thenbb elsebb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_br]

opaque Lean.LLVM.buildBr {ctx : Context} (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_alloca]

opaque Lean.LLVM.buildAlloca {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_load2]

opaque Lean.LLVM.buildLoad2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (val : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_store]

opaque Lean.LLVM.buildStore {ctx : Context} (builder : Builder ctx) (val store_loc_ptr : Value ctx) : BaseIO Unit

@[extern lean_llvm_build_ret]

opaque Lean.LLVM.buildRet {ctx : Context} (builder : Builder ctx) (val : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_unreachable]

opaque Lean.LLVM.buildUnreachable {ctx : Context} (builder : Builder ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_gep2]

opaque Lean.LLVM.buildGEP2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (base : Value ctx) (ixs : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_inbounds_gep2]

opaque Lean.LLVM.buildInBoundsGEP2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (base : Value ctx) (ixs : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sext]

opaque Lean.LLVM.buildSext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_zext]

opaque Lean.LLVM.buildZext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sext_or_trunc]

opaque Lean.LLVM.buildSextOrTrunc {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_switch]

opaque Lean.LLVM.buildSwitch {ctx : Context} (builder : Builder ctx) (val : Value ctx) (elseBB : BasicBlock ctx) (numCasesHint : UInt64) : BaseIO (Value ctx)

@[extern lean_llvm_build_ptr_to_int]

opaque Lean.LLVM.buildPtrToInt {ctx : Context} (builder : Builder ctx) (ptr : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_mul]

opaque Lean.LLVM.buildMul {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_add]

opaque Lean.LLVM.buildAdd {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sub]

opaque Lean.LLVM.buildSub {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_not]

opaque Lean.LLVM.buildNot {ctx : Context} (builder : Builder ctx) (x : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_icmp]

opaque Lean.LLVM.buildICmp {ctx : Context} (builder : Builder ctx) (predicate : IntPredicate) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_add_case]

opaque Lean.LLVM.addCase {ctx : Context} (switch onVal : Value ctx) (destBB : BasicBlock ctx) : BaseIO Unit

@[extern lean_llvm_get_insert_block]

opaque Lean.LLVM.getInsertBlock {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_clear_insertion_position]

opaque Lean.LLVM.clearInsertionPosition {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) : BaseIO Unit

@[extern lean_llvm_get_basic_block_parent]

opaque Lean.LLVM.getBasicBlockParent {ctx : Context} (bb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_type_of]

opaque Lean.LLVM.typeOf {ctx : Context} (val : Value ctx) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_int]

opaque Lean.LLVM.constInt {ctx : Context} (intty : LLVMType ctx) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

@[extern lean_llvm_print_module_to_string]

opaque Lean.LLVM.printModuletoString {ctx : Context} (mod : Module ctx) : BaseIO String

@[extern lean_llvm_print_module_to_file]

opaque Lean.LLVM.printModuletoFile {ctx : Context} (mod : Module ctx) (file : String) : BaseIO Unit

@[extern llvm_count_params]

opaque Lean.LLVM.countParams {ctx : Context} (fn : Value ctx) : BaseIO UInt64

@[extern llvm_get_param]

opaque Lean.LLVM.getParam {ctx : Context} (fn : Value ctx) (ix : UInt64) : BaseIO (Value ctx)

@[extern lean_llvm_create_memory_buffer_with_contents_of_file]

opaque Lean.LLVM.createMemoryBufferWithContentsOfFile {ctx : Context} (path : String) : BaseIO (MemoryBuffer ctx)

@[extern lean_llvm_parse_bitcode]

opaque Lean.LLVM.parseBitcode (ctx : Context) (membuf : MemoryBuffer ctx) : BaseIO (Module ctx)

@[extern lean_llvm_link_modules]

opaque Lean.LLVM.linkModules {ctx : Context} (dest src : Module ctx) : BaseIO Unit

@[extern lean_llvm_get_default_target_triple]

opaque Lean.LLVM.getDefaultTargetTriple : BaseIO String

@[extern lean_llvm_get_target_from_triple]

opaque Lean.LLVM.getTargetFromTriple {ctx : Context} (triple : String) : BaseIO (Target ctx)

@[extern lean_llvm_create_target_machine]

opaque Lean.LLVM.createTargetMachine {ctx : Context} (target : Target ctx) (tripleStr cpu features : String) : BaseIO (TargetMachine ctx)

@[extern lean_llvm_target_machine_emit_to_file]

opaque Lean.LLVM.targetMachineEmitToFile {ctx : Context} (targetMachine : TargetMachine ctx) (module : Module ctx) (filepath : String) (codegenType : CodegenFileType) : BaseIO Unit

@[extern lean_llvm_dispose_target_machine]

opaque Lean.LLVM.disposeTargetMachine {ctx : Context} (tm : TargetMachine ctx) : BaseIO Unit

@[extern lean_llvm_dispose_module]

opaque Lean.LLVM.disposeModule {ctx : Context} (m : Module ctx) : BaseIO Unit

@[extern lean_llvm_verify_module]

opaque Lean.LLVM.verifyModule {ctx : Context} (m : Module ctx) : BaseIO (Option String)

@[extern lean_llvm_create_string_attribute]

opaque Lean.LLVM.createStringAttribute {ctx : Context} (key value : String) : BaseIO (Attribute ctx)

@[extern lean_llvm_add_attribute_at_index]

opaque Lean.LLVM.addAttributeAtIndex {ctx : Context} (fn : Value ctx) (idx : AttributeIndex) (attr : Attribute ctx) : BaseIO Unit

structure Lean.LLVM.Visibility : Type

• val : UInt64

def Lean.LLVM.Visibility.default : Visibility

Equations

• Lean.LLVM.Visibility.default = { val := 0 }

def Lean.LLVM.Visibility.hidden : Visibility

Equations

• Lean.LLVM.Visibility.hidden = { val := 1 }

def Lean.LLVM.Visibility.protected : Visibility

Equations

• Lean.LLVM.Visibility.protected = { val := 2 }

@[extern lean_llvm_set_visibility]

opaque Lean.LLVM.setVisibility {ctx : Context} (value : Value ctx) (visibility : Visibility) : BaseIO Unit

structure Lean.LLVM.DLLStorageClass : Type

• val : UInt64

def Lean.LLVM.DLLStorageClass.default : DLLStorageClass

Equations

• Lean.LLVM.DLLStorageClass.default = { val := 0 }

def Lean.LLVM.DLLStorageClass.import : DLLStorageClass

Equations

• Lean.LLVM.DLLStorageClass.import = { val := 1 }

def Lean.LLVM.DLLStorageClass.export : DLLStorageClass

Equations

• Lean.LLVM.DLLStorageClass.export = { val := 2 }

@[extern lean_llvm_set_dll_storage_class]

opaque Lean.LLVM.setDLLStorageClass {ctx : Context} (value : Value ctx) (dllStorageClass : DLLStorageClass) : BaseIO Unit

structure Lean.LLVM.Linkage : Type

• val : UInt64

def Lean.LLVM.Linkage.external : Linkage

Externally visible function

Equations

• Lean.LLVM.Linkage.external = { val := 0 }

def Lean.LLVM.Linkage.availableExternally : Linkage

Equations

• Lean.LLVM.Linkage.availableExternally = { val := 1 }

def Lean.LLVM.Linkage.linkOnceAny : Linkage

Keep one copy of function when linking (inline)

Equations

• Lean.LLVM.Linkage.linkOnceAny = { val := 2 }

def Lean.LLVM.Linkage.linkOnceODR : Linkage

Same, but only replaced by something equivalent

Equations

• Lean.LLVM.Linkage.linkOnceODR = { val := 3 }

def Lean.LLVM.Linkage.linkOnceODRAutoHide : Linkage

Obsolete

Equations

• Lean.LLVM.Linkage.linkOnceODRAutoHide = { val := 4 }

def Lean.LLVM.Linkage.weakAny : Linkage

Keep one copy of function when linking (weak)

Equations

• Lean.LLVM.Linkage.weakAny = { val := 5 }

def Lean.LLVM.Linkage.weakODR : Linkage

Same, but only replaced by something equivalent

Equations

• Lean.LLVM.Linkage.weakODR = { val := 6 }

def Lean.LLVM.Linkage.appending : Linkage

Special purpose, only applies to global arrays

Equations

• Lean.LLVM.Linkage.appending = { val := 7 }

def Lean.LLVM.Linkage.internal : Linkage

Rename collisions when linking (static functions)

Equations

• Lean.LLVM.Linkage.internal = { val := 8 }

def Lean.LLVM.Linkage.private : Linkage

Like Internal, but omit from symbol table

Equations

• Lean.LLVM.Linkage.private = { val := 9 }

def Lean.LLVM.Linkage.dllImport : Linkage

Obsolete

Equations

• Lean.LLVM.Linkage.dllImport = { val := 10 }

def Lean.LLVM.Linkage.dllExport : Linkage

Obsolete

Equations

• Lean.LLVM.Linkage.dllExport = { val := 11 }

def Lean.LLVM.Linkage.externalWeak : Linkage

ExternalWeak linkage description

Equations

• Lean.LLVM.Linkage.externalWeak = { val := 12 }

def Lean.LLVM.Linkage.ghost : Linkage

Obsolete

Equations

• Lean.LLVM.Linkage.ghost = { val := 13 }

def Lean.LLVM.Linkage.common : Linkage

Tentative definitions

Equations

• Lean.LLVM.Linkage.common = { val := 14 }

def Lean.LLVM.Linkage.linkerPrivate : Linkage

Like Private, but linker removes.

Equations

• Lean.LLVM.Linkage.linkerPrivate = { val := 15 }

def Lean.LLVM.Linkage.linkerPrivateWeak : Linkage

Like LinkerPrivate, but is weak.

Equations

• Lean.LLVM.Linkage.linkerPrivateWeak = { val := 16 }

@[extern lean_llvm_set_linkage]

opaque Lean.LLVM.setLinkage {ctx : Context} (value : Value ctx) (linkage : Linkage) : BaseIO Unit

def Lean.LLVM.i1Type (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i1Type ctx = Lean.LLVM.intTypeInContext ctx 1

def Lean.LLVM.i8Type (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i8Type ctx = Lean.LLVM.intTypeInContext ctx 8

def Lean.LLVM.i16Type (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i16Type ctx = Lean.LLVM.intTypeInContext ctx 16

def Lean.LLVM.i32Type (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i32Type ctx = Lean.LLVM.intTypeInContext ctx 32

def Lean.LLVM.i64Type (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i64Type ctx = Lean.LLVM.intTypeInContext ctx 64

def Lean.LLVM.voidPtrType (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.voidPtrType ctx = do let __do_lift ← Lean.LLVM.intTypeInContext ctx 8 Lean.LLVM.pointerType __do_lift

def Lean.LLVM.i8PtrType (ctx : Context) : BaseIO (LLVMType ctx)

Equations

• Lean.LLVM.i8PtrType ctx = Lean.LLVM.voidPtrType ctx

def Lean.LLVM.constTrue (ctx : Context) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constTrue ctx = do let __do_lift ← Lean.LLVM.i1Type ctx Lean.LLVM.constInt __do_lift 1

def Lean.LLVM.constFalse (ctx : Context) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constFalse ctx = do let __do_lift ← Lean.LLVM.i1Type ctx Lean.LLVM.constInt __do_lift 0

def Lean.LLVM.constInt' (ctx : Context) (width value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constInt' ctx width value signExtend = do let __do_lift ← Lean.LLVM.intTypeInContext ctx width Lean.LLVM.constInt __do_lift value signExtend

def Lean.LLVM.constInt1 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constInt1 ctx value signExtend = Lean.LLVM.constInt' ctx 1 value signExtend

def Lean.LLVM.constInt8 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constInt8 ctx value signExtend = Lean.LLVM.constInt' ctx 8 value signExtend

def Lean.LLVM.constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constInt32 ctx value signExtend = Lean.LLVM.constInt' ctx 32 value signExtend

def Lean.LLVM.constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constInt64 ctx value signExtend = Lean.LLVM.constInt' ctx 64 value signExtend

def Lean.LLVM.constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constIntSizeT ctx value signExtend = Lean.LLVM.constInt' ctx 64 value signExtend

def Lean.LLVM.constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

Equations

• Lean.LLVM.constIntUnsigned ctx value signExtend = Lean.LLVM.constInt' ctx 32 value signExtend