Documentation

Batteries.Data.UInt

UInt8 #

theorem UInt8.ext_iff {x : UInt8} {y : UInt8} :
x = y x.toNat = y.toNat
theorem UInt8.ext {x : UInt8} {y : UInt8} :
x.toNat = y.toNatx = y
@[simp]
theorem UInt8.val_val_eq_toNat (x : UInt8) :
x.val = x.toNat
@[simp]
theorem UInt8.val_ofNat (n : Nat) :
@[simp]
theorem UInt8.toNat_ofNat (n : Nat) :
theorem UInt8.toNat_lt (x : UInt8) :
x.toNat < 2 ^ 8
@[simp]
theorem UInt8.toUInt16_toNat (x : UInt8) :
x.toUInt16.toNat = x.toNat
@[simp]
theorem UInt8.toUInt32_toNat (x : UInt8) :
x.toUInt32.toNat = x.toNat
@[simp]
theorem UInt8.toUInt64_toNat (x : UInt8) :
x.toUInt64.toNat = x.toNat
theorem UInt8.toNat_add (x : UInt8) (y : UInt8) :
(x + y).toNat = (x.toNat + y.toNat) % UInt8.size
theorem UInt8.toNat_sub (x : UInt8) (y : UInt8) :
(x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size
theorem UInt8.toNat_mul (x : UInt8) (y : UInt8) :
(x * y).toNat = x.toNat * y.toNat % UInt8.size
theorem UInt8.toNat_div (x : UInt8) (y : UInt8) :
(x / y).toNat = x.toNat / y.toNat
theorem UInt8.toNat_mod (x : UInt8) (y : UInt8) :
(x % y).toNat = x.toNat % y.toNat
theorem UInt8.toNat_modn (x : UInt8) (n : Nat) :
(x.modn n).toNat = x.toNat % n
theorem UInt8.le_antisymm_iff {x : UInt8} {y : UInt8} :
x = y x y y x
theorem UInt8.le_antisymm {x : UInt8} {y : UInt8} (h1 : x y) (h2 : y x) :
x = y

UInt16 #

theorem UInt16.ext_iff {x : UInt16} {y : UInt16} :
x = y x.toNat = y.toNat
theorem UInt16.ext {x : UInt16} {y : UInt16} :
x.toNat = y.toNatx = y
@[simp]
theorem UInt16.val_val_eq_toNat (x : UInt16) :
x.val = x.toNat
@[simp]
theorem UInt16.val_ofNat (n : Nat) :
@[simp]
theorem UInt16.toNat_ofNat (n : Nat) :
theorem UInt16.toNat_lt (x : UInt16) :
x.toNat < 2 ^ 16
@[simp]
theorem UInt16.toUInt8_toNat (x : UInt16) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt16.toUInt32_toNat (x : UInt16) :
x.toUInt32.toNat = x.toNat
@[simp]
theorem UInt16.toUInt64_toNat (x : UInt16) :
x.toUInt64.toNat = x.toNat
theorem UInt16.toNat_add (x : UInt16) (y : UInt16) :
(x + y).toNat = (x.toNat + y.toNat) % UInt16.size
theorem UInt16.toNat_sub (x : UInt16) (y : UInt16) :
(x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size
theorem UInt16.toNat_mul (x : UInt16) (y : UInt16) :
(x * y).toNat = x.toNat * y.toNat % UInt16.size
theorem UInt16.toNat_div (x : UInt16) (y : UInt16) :
(x / y).toNat = x.toNat / y.toNat
theorem UInt16.toNat_mod (x : UInt16) (y : UInt16) :
(x % y).toNat = x.toNat % y.toNat
theorem UInt16.toNat_modn (x : UInt16) (n : Nat) :
(x.modn n).toNat = x.toNat % n
theorem UInt16.le_antisymm_iff {x : UInt16} {y : UInt16} :
x = y x y y x
theorem UInt16.le_antisymm {x : UInt16} {y : UInt16} (h1 : x y) (h2 : y x) :
x = y

UInt32 #

theorem UInt32.ext_iff {x : UInt32} {y : UInt32} :
x = y x.toNat = y.toNat
theorem UInt32.ext {x : UInt32} {y : UInt32} :
x.toNat = y.toNatx = y
@[simp]
theorem UInt32.val_val_eq_toNat (x : UInt32) :
x.val = x.toNat
@[simp]
theorem UInt32.val_ofNat (n : Nat) :
@[simp]
theorem UInt32.toNat_ofNat (n : Nat) :
theorem UInt32.toNat_lt (x : UInt32) :
x.toNat < 2 ^ 32
@[simp]
theorem UInt32.toUInt8_toNat (x : UInt32) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt32.toUInt16_toNat (x : UInt32) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
@[simp]
theorem UInt32.toUInt64_toNat (x : UInt32) :
x.toUInt64.toNat = x.toNat
theorem UInt32.toNat_add (x : UInt32) (y : UInt32) :
(x + y).toNat = (x.toNat + y.toNat) % UInt32.size
theorem UInt32.toNat_sub (x : UInt32) (y : UInt32) :
(x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size
theorem UInt32.toNat_mul (x : UInt32) (y : UInt32) :
(x * y).toNat = x.toNat * y.toNat % UInt32.size
theorem UInt32.toNat_div (x : UInt32) (y : UInt32) :
(x / y).toNat = x.toNat / y.toNat
theorem UInt32.toNat_mod (x : UInt32) (y : UInt32) :
(x % y).toNat = x.toNat % y.toNat
theorem UInt32.toNat_modn (x : UInt32) (n : Nat) :
(x.modn n).toNat = x.toNat % n
theorem UInt32.le_antisymm_iff {x : UInt32} {y : UInt32} :
x = y x y y x
theorem UInt32.le_antisymm {x : UInt32} {y : UInt32} (h1 : x y) (h2 : y x) :
x = y

UInt64 #

theorem UInt64.ext_iff {x : UInt64} {y : UInt64} :
x = y x.toNat = y.toNat
theorem UInt64.ext {x : UInt64} {y : UInt64} :
x.toNat = y.toNatx = y
@[simp]
theorem UInt64.val_val_eq_toNat (x : UInt64) :
x.val = x.toNat
@[simp]
theorem UInt64.val_ofNat (n : Nat) :
@[simp]
theorem UInt64.toNat_ofNat (n : Nat) :
theorem UInt64.toNat_lt (x : UInt64) :
x.toNat < 2 ^ 64
@[simp]
theorem UInt64.toUInt8_toNat (x : UInt64) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
@[simp]
theorem UInt64.toUInt16_toNat (x : UInt64) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
@[simp]
theorem UInt64.toUInt32_toNat (x : UInt64) :
x.toUInt32.toNat = x.toNat % 2 ^ 32
theorem UInt64.toNat_add (x : UInt64) (y : UInt64) :
(x + y).toNat = (x.toNat + y.toNat) % UInt64.size
theorem UInt64.toNat_sub (x : UInt64) (y : UInt64) :
(x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size
theorem UInt64.toNat_mul (x : UInt64) (y : UInt64) :
(x * y).toNat = x.toNat * y.toNat % UInt64.size
theorem UInt64.toNat_div (x : UInt64) (y : UInt64) :
(x / y).toNat = x.toNat / y.toNat
theorem UInt64.toNat_mod (x : UInt64) (y : UInt64) :
(x % y).toNat = x.toNat % y.toNat
theorem UInt64.toNat_modn (x : UInt64) (n : Nat) :
(x.modn n).toNat = x.toNat % n
theorem UInt64.le_antisymm_iff {x : UInt64} {y : UInt64} :
x = y x y y x
theorem UInt64.le_antisymm {x : UInt64} {y : UInt64} (h1 : x y) (h2 : y x) :
x = y

USize #

theorem USize.ext_iff {x : USize} {y : USize} :
x = y x.toNat = y.toNat
theorem USize.ext {x : USize} {y : USize} :
x.toNat = y.toNatx = y
@[simp]
theorem USize.val_val_eq_toNat (x : USize) :
x.val = x.toNat
@[simp]
theorem USize.val_ofNat (n : Nat) :
@[simp]
theorem USize.toNat_ofNat (n : Nat) :
@[simp]
theorem USize.toUInt64_toNat (x : USize) :
x.toUInt64.toNat = x.toNat
@[simp]
theorem UInt32.toUSize_toNat (x : UInt32) :
x.toUSize.toNat = x.toNat
theorem USize.toNat_add (x : USize) (y : USize) :
(x + y).toNat = (x.toNat + y.toNat) % USize.size
theorem USize.toNat_sub (x : USize) (y : USize) :
(x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size
theorem USize.toNat_mul (x : USize) (y : USize) :
(x * y).toNat = x.toNat * y.toNat % USize.size
theorem USize.toNat_div (x : USize) (y : USize) :
(x / y).toNat = x.toNat / y.toNat
theorem USize.toNat_mod (x : USize) (y : USize) :
(x % y).toNat = x.toNat % y.toNat
theorem USize.toNat_modn (x : USize) (n : Nat) :
(x.modn n).toNat = x.toNat % n
theorem USize.le_antisymm_iff {x : USize} {y : USize} :
x = y x y y x
theorem USize.le_antisymm {x : USize} {y : USize} (h1 : x y) (h2 : y x) :
x = y