Documentation

Init.Data.UInt.Basic

@[extern lean_uint8_add]
def UInt8.add (a b : UInt8) :
Equations
@[extern lean_uint8_sub]
def UInt8.sub (a b : UInt8) :
Equations
@[extern lean_uint8_mul]
def UInt8.mul (a b : UInt8) :
Equations
@[extern lean_uint8_div]
def UInt8.div (a b : UInt8) :
Equations
@[extern lean_uint8_mod]
def UInt8.mod (a b : UInt8) :
Equations
@[deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.modn (a : UInt8) (n : Nat) :
Equations
@[extern lean_uint8_land]
def UInt8.land (a b : UInt8) :
Equations
@[extern lean_uint8_lor]
def UInt8.lor (a b : UInt8) :
Equations
@[extern lean_uint8_xor]
def UInt8.xor (a b : UInt8) :
Equations
@[extern lean_uint8_shift_left]
Equations
@[extern lean_uint8_shift_right]
Equations
def UInt8.lt (a b : UInt8) :
Equations
def UInt8.le (a b : UInt8) :
Equations
Equations
Equations
Equations
Equations
Equations
instance instLTUInt8 :
Equations
instance instLEUInt8 :
Equations
@[extern lean_uint8_complement]
Equations
Equations
@[extern lean_bool_to_uint8]
Equations
@[extern lean_uint8_dec_lt]
def UInt8.decLt (a b : UInt8) :
Decidable (a < b)
Equations
@[extern lean_uint8_dec_le]
def UInt8.decLe (a b : UInt8) :
Equations
instance instDecidableLtUInt8 (a b : UInt8) :
Decidable (a < b)
Equations
instance instDecidableLeUInt8 (a b : UInt8) :
Equations
@[extern lean_uint16_add]
def UInt16.add (a b : UInt16) :
Equations
@[extern lean_uint16_sub]
def UInt16.sub (a b : UInt16) :
Equations
@[extern lean_uint16_mul]
def UInt16.mul (a b : UInt16) :
Equations
@[extern lean_uint16_div]
def UInt16.div (a b : UInt16) :
Equations
@[extern lean_uint16_mod]
def UInt16.mod (a b : UInt16) :
Equations
@[deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.modn (a : UInt16) (n : Nat) :
Equations
@[extern lean_uint16_land]
Equations
@[extern lean_uint16_lor]
def UInt16.lor (a b : UInt16) :
Equations
@[extern lean_uint16_xor]
def UInt16.xor (a b : UInt16) :
Equations
@[extern lean_uint16_shift_left]
Equations
@[extern lean_uint16_shift_right]
Equations
def UInt16.lt (a b : UInt16) :
Equations
def UInt16.le (a b : UInt16) :
Equations
Equations
Equations
@[extern lean_uint16_complement]
Equations
@[extern lean_bool_to_uint16]
Equations
@[extern lean_uint16_dec_lt]
def UInt16.decLt (a b : UInt16) :
Decidable (a < b)
Equations
@[extern lean_uint16_dec_le]
def UInt16.decLe (a b : UInt16) :
Equations
@[extern lean_uint32_add]
def UInt32.add (a b : UInt32) :
Equations
@[extern lean_uint32_sub]
def UInt32.sub (a b : UInt32) :
Equations
@[extern lean_uint32_mul]
def UInt32.mul (a b : UInt32) :
Equations
@[extern lean_uint32_div]
def UInt32.div (a b : UInt32) :
Equations
@[extern lean_uint32_mod]
def UInt32.mod (a b : UInt32) :
Equations
@[deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.modn (a : UInt32) (n : Nat) :
Equations
@[extern lean_uint32_land]
Equations
@[extern lean_uint32_lor]
def UInt32.lor (a b : UInt32) :
Equations
@[extern lean_uint32_xor]
def UInt32.xor (a b : UInt32) :
Equations
@[extern lean_uint32_shift_left]
Equations
@[extern lean_uint32_shift_right]
Equations
def UInt32.lt (a b : UInt32) :
Equations
def UInt32.le (a b : UInt32) :
Equations
@[extern lean_uint32_complement]
Equations
@[extern lean_bool_to_uint32]
Equations
@[extern lean_uint64_add]
def UInt64.add (a b : UInt64) :
Equations
@[extern lean_uint64_sub]
def UInt64.sub (a b : UInt64) :
Equations
@[extern lean_uint64_mul]
def UInt64.mul (a b : UInt64) :
Equations
@[extern lean_uint64_div]
def UInt64.div (a b : UInt64) :
Equations
@[extern lean_uint64_mod]
def UInt64.mod (a b : UInt64) :
Equations
@[deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.modn (a : UInt64) (n : Nat) :
Equations
@[extern lean_uint64_land]
Equations
@[extern lean_uint64_lor]
def UInt64.lor (a b : UInt64) :
Equations
@[extern lean_uint64_xor]
def UInt64.xor (a b : UInt64) :
Equations
@[extern lean_uint64_shift_left]
Equations
@[extern lean_uint64_shift_right]
Equations
def UInt64.lt (a b : UInt64) :
Equations
def UInt64.le (a b : UInt64) :
Equations
Equations
Equations
@[extern lean_uint64_complement]
Equations
@[extern lean_bool_to_uint64]
Equations
@[extern lean_uint64_dec_lt]
def UInt64.decLt (a b : UInt64) :
Decidable (a < b)
Equations
@[extern lean_uint64_dec_le]
def UInt64.decLe (a b : UInt64) :
Equations
theorem usize_size_le :
USize.size 18446744073709551616
theorem le_usize_size :
4294967296 USize.size
@[extern lean_usize_mul]
def USize.mul (a b : USize) :
Equations
@[extern lean_usize_div]
def USize.div (a b : USize) :
Equations
@[extern lean_usize_mod]
def USize.mod (a b : USize) :
Equations
@[deprecated USize.mod (since := "2024-09-23")]
def USize.modn (a : USize) (n : Nat) :
Equations
@[extern lean_usize_land]
def USize.land (a b : USize) :
Equations
@[extern lean_usize_lor]
def USize.lor (a b : USize) :
Equations
@[extern lean_usize_xor]
def USize.xor (a b : USize) :
Equations
@[extern lean_usize_shift_left]
Equations
@[extern lean_usize_shift_right]
Equations
@[extern lean_usize_of_nat]
def USize.ofNat32 (n : Nat) (h : n < 4294967296) :

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
@[extern lean_uint8_to_usize]
Equations
@[extern lean_usize_to_uint8]
Equations
@[extern lean_uint16_to_usize]
Equations
@[extern lean_usize_to_uint16]
Equations
@[extern lean_uint32_to_usize]
Equations
@[extern lean_usize_to_uint32]
Equations
@[extern lean_uint64_to_usize]

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

Equations
@[extern lean_usize_to_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
Equations
Equations
Equations
@[extern lean_usize_complement]
Equations
Equations
@[extern lean_bool_to_usize]
Equations