@[extern lean_uint8_add]

def UInt8.add (a b : UInt8) : UInt8

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint8_sub]

def UInt8.sub (a b : UInt8) : UInt8

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint8_mul]

def UInt8.mul (a b : UInt8) : UInt8

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint8_div]

def UInt8.div (a b : UInt8) : UInt8

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint8_mod]

def UInt8.mod (a b : UInt8) : UInt8

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt8.mod]

def UInt8.modn (a : UInt8) (n : Nat) : UInt8

Equations

• a.modn n = { toBitVec := ↑↑(a.val.modn n) }

@[extern lean_uint8_land]

def UInt8.land (a b : UInt8) : UInt8

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint8_lor]

def UInt8.lor (a b : UInt8) : UInt8

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint8_xor]

def UInt8.xor (a b : UInt8) : UInt8

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint8_shift_left]

def UInt8.shiftLeft (a b : UInt8) : UInt8

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 8).toBitVec }

@[extern lean_uint8_shift_right]

def UInt8.shiftRight (a b : UInt8) : UInt8

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 8).toBitVec }

def UInt8.lt (a b : UInt8) : Prop

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt8.le (a b : UInt8) : Prop

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt8 : Add UInt8

Equations

• instAddUInt8 = { add := UInt8.add }

instance instSubUInt8 : Sub UInt8

Equations

• instSubUInt8 = { sub := UInt8.sub }

instance instMulUInt8 : Mul UInt8

Equations

• instMulUInt8 = { mul := UInt8.mul }

instance instModUInt8 : Mod UInt8

Equations

• instModUInt8 = { mod := UInt8.mod }

instance instHModUInt8Nat : HMod UInt8 Nat UInt8

Equations

• instHModUInt8Nat = { hMod := UInt8.modn }

instance instDivUInt8 : Div UInt8

Equations

• instDivUInt8 = { div := UInt8.div }

instance instLTUInt8 : LT UInt8

Equations

• instLTUInt8 = { lt := UInt8.lt }

instance instLEUInt8 : LE UInt8

Equations

• instLEUInt8 = { le := UInt8.le }

@[extern lean_uint8_complement]

def UInt8.complement (a : UInt8) : UInt8

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

instance instComplementUInt8 : Complement UInt8

Equations

• instComplementUInt8 = { complement := UInt8.complement }

instance instAndOpUInt8 : AndOp UInt8

Equations

• instAndOpUInt8 = { and := UInt8.land }

instance instOrOpUInt8 : OrOp UInt8

Equations

• instOrOpUInt8 = { or := UInt8.lor }

instance instXorUInt8 : Xor UInt8

Equations

• instXorUInt8 = { xor := UInt8.xor }

instance instShiftLeftUInt8 : ShiftLeft UInt8

Equations

• instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }

instance instShiftRightUInt8 : ShiftRight UInt8

Equations

• instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }

@[extern lean_bool_to_uint8]

def Bool.toUInt8 (b : Bool) : UInt8

Equations

• b.toUInt8 = if b = true then 1 else 0

@[extern lean_uint8_dec_lt]

def UInt8.decLt (a b : UInt8) : Decidable (a < b)

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint8_dec_le]

def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b)

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt8 (a b : UInt8) : Decidable (a < b)

Equations

• instDecidableLtUInt8 a b = a.decLt b

instance instDecidableLeUInt8 (a b : UInt8) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt8 a b = a.decLe b

instance instMaxUInt8 : Max UInt8

Equations

• instMaxUInt8 = maxOfLe

instance instMinUInt8 : Min UInt8

Equations

• instMinUInt8 = minOfLe

@[extern lean_uint16_add]

def UInt16.add (a b : UInt16) : UInt16

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint16_sub]

def UInt16.sub (a b : UInt16) : UInt16

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint16_mul]

def UInt16.mul (a b : UInt16) : UInt16

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint16_div]

def UInt16.div (a b : UInt16) : UInt16

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint16_mod]

def UInt16.mod (a b : UInt16) : UInt16

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt16.mod]

def UInt16.modn (a : UInt16) (n : Nat) : UInt16

Equations

• a.modn n = { toBitVec := ↑↑(a.val.modn n) }

@[extern lean_uint16_land]

def UInt16.land (a b : UInt16) : UInt16

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint16_lor]

def UInt16.lor (a b : UInt16) : UInt16

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint16_xor]

def UInt16.xor (a b : UInt16) : UInt16

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint16_shift_left]

def UInt16.shiftLeft (a b : UInt16) : UInt16

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 16).toBitVec }

@[extern lean_uint16_shift_right]

def UInt16.shiftRight (a b : UInt16) : UInt16

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 16).toBitVec }

def UInt16.lt (a b : UInt16) : Prop

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt16.le (a b : UInt16) : Prop

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt16 : Add UInt16

Equations

• instAddUInt16 = { add := UInt16.add }

instance instSubUInt16 : Sub UInt16

Equations

• instSubUInt16 = { sub := UInt16.sub }

instance instMulUInt16 : Mul UInt16

Equations

• instMulUInt16 = { mul := UInt16.mul }

instance instModUInt16 : Mod UInt16

Equations

• instModUInt16 = { mod := UInt16.mod }

instance instHModUInt16Nat : HMod UInt16 Nat UInt16

Equations

• instHModUInt16Nat = { hMod := UInt16.modn }

instance instDivUInt16 : Div UInt16

Equations

• instDivUInt16 = { div := UInt16.div }

instance instLTUInt16 : LT UInt16

Equations

• instLTUInt16 = { lt := UInt16.lt }

instance instLEUInt16 : LE UInt16

Equations

• instLEUInt16 = { le := UInt16.le }

@[extern lean_uint16_complement]

def UInt16.complement (a : UInt16) : UInt16

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

instance instComplementUInt16 : Complement UInt16

Equations

• instComplementUInt16 = { complement := UInt16.complement }

instance instAndOpUInt16 : AndOp UInt16

Equations

• instAndOpUInt16 = { and := UInt16.land }

instance instOrOpUInt16 : OrOp UInt16

Equations

• instOrOpUInt16 = { or := UInt16.lor }

instance instXorUInt16 : Xor UInt16

Equations

• instXorUInt16 = { xor := UInt16.xor }

instance instShiftLeftUInt16 : ShiftLeft UInt16

Equations

• instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }

instance instShiftRightUInt16 : ShiftRight UInt16

Equations

• instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }

@[extern lean_bool_to_uint16]

def Bool.toUInt16 (b : Bool) : UInt16

Equations

• b.toUInt16 = if b = true then 1 else 0

@[extern lean_uint16_dec_lt]

def UInt16.decLt (a b : UInt16) : Decidable (a < b)

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint16_dec_le]

def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b)

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt16 (a b : UInt16) : Decidable (a < b)

Equations

• instDecidableLtUInt16 a b = a.decLt b

instance instDecidableLeUInt16 (a b : UInt16) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt16 a b = a.decLe b

instance instMaxUInt16 : Max UInt16

Equations

• instMaxUInt16 = maxOfLe

instance instMinUInt16 : Min UInt16

Equations

• instMinUInt16 = minOfLe

@[extern lean_uint32_add]

def UInt32.add (a b : UInt32) : UInt32

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint32_sub]

def UInt32.sub (a b : UInt32) : UInt32

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint32_mul]

def UInt32.mul (a b : UInt32) : UInt32

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint32_div]

def UInt32.div (a b : UInt32) : UInt32

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint32_mod]

def UInt32.mod (a b : UInt32) : UInt32

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt32.mod]

def UInt32.modn (a : UInt32) (n : Nat) : UInt32

Equations

• a.modn n = { toBitVec := ↑↑(a.val.modn n) }

@[extern lean_uint32_land]

def UInt32.land (a b : UInt32) : UInt32

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint32_lor]

def UInt32.lor (a b : UInt32) : UInt32

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint32_xor]

def UInt32.xor (a b : UInt32) : UInt32

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint32_shift_left]

def UInt32.shiftLeft (a b : UInt32) : UInt32

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 32).toBitVec }

@[extern lean_uint32_shift_right]

def UInt32.shiftRight (a b : UInt32) : UInt32

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 32).toBitVec }

instance instAddUInt32 : Add UInt32

Equations

• instAddUInt32 = { add := UInt32.add }

instance instSubUInt32 : Sub UInt32

Equations

• instSubUInt32 = { sub := UInt32.sub }

instance instMulUInt32 : Mul UInt32

Equations

• instMulUInt32 = { mul := UInt32.mul }

instance instModUInt32 : Mod UInt32

Equations

• instModUInt32 = { mod := UInt32.mod }

instance instHModUInt32Nat : HMod UInt32 Nat UInt32

Equations

• instHModUInt32Nat = { hMod := UInt32.modn }

instance instDivUInt32 : Div UInt32

Equations

• instDivUInt32 = { div := UInt32.div }

@[extern lean_uint32_complement]

def UInt32.complement (a : UInt32) : UInt32

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

instance instComplementUInt32 : Complement UInt32

Equations

• instComplementUInt32 = { complement := UInt32.complement }

instance instAndOpUInt32 : AndOp UInt32

Equations

• instAndOpUInt32 = { and := UInt32.land }

instance instOrOpUInt32 : OrOp UInt32

Equations

• instOrOpUInt32 = { or := UInt32.lor }

instance instXorUInt32 : Xor UInt32

Equations

• instXorUInt32 = { xor := UInt32.xor }

instance instShiftLeftUInt32 : ShiftLeft UInt32

Equations

• instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }

instance instShiftRightUInt32 : ShiftRight UInt32

Equations

• instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }

@[extern lean_bool_to_uint32]

def Bool.toUInt32 (b : Bool) : UInt32

Equations

• b.toUInt32 = if b = true then 1 else 0

@[extern lean_uint64_add]

def UInt64.add (a b : UInt64) : UInt64

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint64_sub]

def UInt64.sub (a b : UInt64) : UInt64

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint64_mul]

def UInt64.mul (a b : UInt64) : UInt64

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint64_div]

def UInt64.div (a b : UInt64) : UInt64

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint64_mod]

def UInt64.mod (a b : UInt64) : UInt64

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt64.mod]

def UInt64.modn (a : UInt64) (n : Nat) : UInt64

Equations

• a.modn n = { toBitVec := ↑↑(a.val.modn n) }

@[extern lean_uint64_land]

def UInt64.land (a b : UInt64) : UInt64

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint64_lor]

def UInt64.lor (a b : UInt64) : UInt64

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint64_xor]

def UInt64.xor (a b : UInt64) : UInt64

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint64_shift_left]

def UInt64.shiftLeft (a b : UInt64) : UInt64

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 64).toBitVec }

@[extern lean_uint64_shift_right]

def UInt64.shiftRight (a b : UInt64) : UInt64

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 64).toBitVec }

def UInt64.lt (a b : UInt64) : Prop

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt64.le (a b : UInt64) : Prop

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt64 : Add UInt64

Equations

• instAddUInt64 = { add := UInt64.add }

instance instSubUInt64 : Sub UInt64

Equations

• instSubUInt64 = { sub := UInt64.sub }

instance instMulUInt64 : Mul UInt64

Equations

• instMulUInt64 = { mul := UInt64.mul }

instance instModUInt64 : Mod UInt64

Equations

• instModUInt64 = { mod := UInt64.mod }

instance instHModUInt64Nat : HMod UInt64 Nat UInt64

Equations

• instHModUInt64Nat = { hMod := UInt64.modn }

instance instDivUInt64 : Div UInt64

Equations

• instDivUInt64 = { div := UInt64.div }

instance instLTUInt64 : LT UInt64

Equations

• instLTUInt64 = { lt := UInt64.lt }

instance instLEUInt64 : LE UInt64

Equations

• instLEUInt64 = { le := UInt64.le }

@[extern lean_uint64_complement]

def UInt64.complement (a : UInt64) : UInt64

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

instance instComplementUInt64 : Complement UInt64

Equations

• instComplementUInt64 = { complement := UInt64.complement }

instance instAndOpUInt64 : AndOp UInt64

Equations

• instAndOpUInt64 = { and := UInt64.land }

instance instOrOpUInt64 : OrOp UInt64

Equations

• instOrOpUInt64 = { or := UInt64.lor }

instance instXorUInt64 : Xor UInt64

Equations

• instXorUInt64 = { xor := UInt64.xor }

instance instShiftLeftUInt64 : ShiftLeft UInt64

Equations

• instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }

instance instShiftRightUInt64 : ShiftRight UInt64

Equations

• instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }

@[extern lean_bool_to_uint64]

def Bool.toUInt64 (b : Bool) : UInt64

Equations

• b.toUInt64 = if b = true then 1 else 0

@[extern lean_uint64_dec_lt]

def UInt64.decLt (a b : UInt64) : Decidable (a < b)

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint64_dec_le]

def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b)

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt64 (a b : UInt64) : Decidable (a < b)

Equations

• instDecidableLtUInt64 a b = a.decLt b

instance instDecidableLeUInt64 (a b : UInt64) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt64 a b = a.decLe b

instance instMaxUInt64 : Max UInt64

Equations

• instMaxUInt64 = maxOfLe

instance instMinUInt64 : Min UInt64

Equations

• instMinUInt64 = minOfLe

theorem usize_size_le : USize.size ≤ 18446744073709551616

theorem le_usize_size : 4294967296 ≤ USize.size

@[extern lean_usize_mul]

def USize.mul (a b : USize) : USize

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_usize_div]

def USize.div (a b : USize) : USize

Equations

• a.div b = { toBitVec := a.toBitVec / b.toBitVec }

@[extern lean_usize_mod]

def USize.mod (a b : USize) : USize

Equations

• a.mod b = { toBitVec := a.toBitVec % b.toBitVec }

@[deprecated USize.mod]

def USize.modn (a : USize) (n : Nat) : USize

Equations

• a.modn n = { toBitVec := ↑↑(a.val.modn n) }

@[extern lean_usize_land]

def USize.land (a b : USize) : USize

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_usize_lor]

def USize.lor (a b : USize) : USize

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_usize_xor]

def USize.xor (a b : USize) : USize

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_usize_shift_left]

def USize.shiftLeft (a b : USize) : USize

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }

@[extern lean_usize_shift_right]

def USize.shiftRight (a b : USize) : USize

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }

@[extern lean_usize_of_nat]

def USize.ofNat32 (n : Nat) (h : n < 4294967296) : USize

Upcast a Nat less than 2^32 to a USize. This is lossless because USize.size is either 2^32 or 2^64. This function is overridden with a native implementation.

Equations

• USize.ofNat32 n h = USize.ofNatCore n ⋯

@[extern lean_uint8_to_usize]

def UInt8.toUSize (a : UInt8) : USize

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint8]

def USize.toUInt8 (a : USize) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint16_to_usize]

def UInt16.toUSize (a : UInt16) : USize

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint16]

def USize.toUInt16 (a : USize) : UInt16

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint32_to_usize]

def UInt32.toUSize (a : UInt32) : USize

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint32]

def USize.toUInt32 (a : USize) : UInt32

Equations

• a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint64_to_usize]

def UInt64.toUSize (a : UInt64) : USize

Converts a UInt64 to a USize by reducing modulo USize.size.

Equations

• a.toUSize = a.toNat.toUSize

@[extern lean_usize_to_uint64]

def USize.toUInt64 (a : USize) : UInt64

Upcast a USize to a UInt64. This is lossless because USize.size is either 2^32 or 2^64. This function is overridden with a native implementation.

Equations

• a.toUInt64 = UInt64.ofNatCore a.toBitVec.toNat ⋯

instance instMulUSize : Mul USize

Equations

• instMulUSize = { mul := USize.mul }

instance instModUSize : Mod USize

Equations

• instModUSize = { mod := USize.mod }

instance instHModUSizeNat : HMod USize Nat USize

Equations

• instHModUSizeNat = { hMod := USize.modn }

instance instDivUSize : Div USize

Equations

• instDivUSize = { div := USize.div }

@[extern lean_usize_complement]

def USize.complement (a : USize) : USize

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

instance instComplementUSize : Complement USize

Equations

• instComplementUSize = { complement := USize.complement }

instance instAndOpUSize : AndOp USize

Equations

• instAndOpUSize = { and := USize.land }

instance instOrOpUSize : OrOp USize

Equations

• instOrOpUSize = { or := USize.lor }

instance instXorUSize : Xor USize

Equations

• instXorUSize = { xor := USize.xor }

instance instShiftLeftUSize : ShiftLeft USize

Equations

• instShiftLeftUSize = { shiftLeft := USize.shiftLeft }

instance instShiftRightUSize : ShiftRight USize

Equations

• instShiftRightUSize = { shiftRight := USize.shiftRight }

@[extern lean_bool_to_usize]

def Bool.toUSize (b : Bool) : USize

Equations

• b.toUSize = if b = true then 1 else 0

instance instMaxUSize : Max USize

Equations

• instMaxUSize = maxOfLe

instance instMinUSize : Min USize

Equations

• instMinUSize = minOfLe