Documentation

Batteries.Data.UInt

UInt8 #

source
theorem UInt8.ext {x : UInt8} {y : UInt8} :
x.toNat = y.toNat → x = y
source
@[simp]
theorem UInt8.val_val_eq_toNat (x : UInt8) :
↑x.val = x.toNat
source
@[simp]
theorem UInt8.toNat_ofNat (n : Nat) :
(OfNat.ofNat n).toNat = n % UInt8.size
source
theorem UInt8.toNat_lt (x : UInt8) :
x.toNat < 2 ^ 8
source
@[simp]
theorem UInt8.toUInt16_toNat (x : UInt8) :
x.toUInt16.toNat = x.toNat
source
@[simp]
theorem UInt8.toUInt32_toNat (x : UInt8) :
x.toUInt32.toNat = x.toNat
source
@[simp]
theorem UInt8.toUInt64_toNat (x : UInt8) :
x.toUInt64.toNat = x.toNat
source
theorem UInt8.toNat_add (x : UInt8) (y : UInt8) :
(x + y).toNat = (x.toNat + y.toNat) % UInt8.size
source
theorem UInt8.toNat_sub (x : UInt8) (y : UInt8) :
(x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size
source
theorem UInt8.toNat_mul (x : UInt8) (y : UInt8) :
(x * y).toNat = x.toNat * y.toNat % UInt8.size
source
theorem UInt8.le_antisymm_iff {x : UInt8} {y : UInt8} :
x = y ↔ x ≤ y ∧ y ≤ x
source
theorem UInt8.le_antisymm {x : UInt8} {y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) :
x = y
source
instance instLawfulOrdUInt8 :
Batteries.LawfulOrd UInt8
Equations

UInt16 #

source
theorem UInt16.ext {x : UInt16} {y : UInt16} :
x.toNat = y.toNat → x = y
source
@[simp]
theorem UInt16.val_val_eq_toNat (x : UInt16) :
↑x.val = x.toNat
source
@[simp]
theorem UInt16.toNat_ofNat (n : Nat) :
(OfNat.ofNat n).toNat = n % UInt16.size
source
theorem UInt16.toNat_lt (x : UInt16) :
x.toNat < 2 ^ 16
source
@[simp]
theorem UInt16.toUInt8_toNat (x : UInt16) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
source
@[simp]
theorem UInt16.toUInt32_toNat (x : UInt16) :
x.toUInt32.toNat = x.toNat
source
@[simp]
theorem UInt16.toUInt64_toNat (x : UInt16) :
x.toUInt64.toNat = x.toNat
source
theorem UInt16.toNat_add (x : UInt16) (y : UInt16) :
(x + y).toNat = (x.toNat + y.toNat) % UInt16.size
source
theorem UInt16.toNat_sub (x : UInt16) (y : UInt16) :
(x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size
source
theorem UInt16.toNat_mul (x : UInt16) (y : UInt16) :
(x * y).toNat = x.toNat * y.toNat % UInt16.size
source
theorem UInt16.le_antisymm_iff {x : UInt16} {y : UInt16} :
x = y ↔ x ≤ y ∧ y ≤ x
source
theorem UInt16.le_antisymm {x : UInt16} {y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) :
x = y
source
instance instLawfulOrdUInt16 :
Batteries.LawfulOrd UInt16
Equations

UInt32 #

source
theorem UInt32.ext {x : UInt32} {y : UInt32} :
x.toNat = y.toNat → x = y
source
@[simp]
theorem UInt32.val_val_eq_toNat (x : UInt32) :
↑x.val = x.toNat
source
@[simp]
theorem UInt32.toNat_ofNat (n : Nat) :
(OfNat.ofNat n).toNat = n % UInt32.size
source
theorem UInt32.toNat_lt (x : UInt32) :
x.toNat < 2 ^ 32
source
@[simp]
theorem UInt32.toUInt8_toNat (x : UInt32) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
source
@[simp]
theorem UInt32.toUInt16_toNat (x : UInt32) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
source
@[simp]
theorem UInt32.toUInt64_toNat (x : UInt32) :
x.toUInt64.toNat = x.toNat
source
theorem UInt32.toNat_add (x : UInt32) (y : UInt32) :
(x + y).toNat = (x.toNat + y.toNat) % UInt32.size
source
theorem UInt32.toNat_sub (x : UInt32) (y : UInt32) :
(x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size
source
theorem UInt32.toNat_mul (x : UInt32) (y : UInt32) :
(x * y).toNat = x.toNat * y.toNat % UInt32.size
source
theorem UInt32.le_antisymm_iff {x : UInt32} {y : UInt32} :
x = y ↔ x ≤ y ∧ y ≤ x
source
theorem UInt32.le_antisymm {x : UInt32} {y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) :
x = y
source
instance instLawfulOrdUInt32 :
Batteries.LawfulOrd UInt32
Equations

UInt64 #

source
theorem UInt64.ext {x : UInt64} {y : UInt64} :
x.toNat = y.toNat → x = y
source
@[simp]
theorem UInt64.val_val_eq_toNat (x : UInt64) :
↑x.val = x.toNat
source
@[simp]
theorem UInt64.toNat_ofNat (n : Nat) :
(OfNat.ofNat n).toNat = n % UInt64.size
source
theorem UInt64.toNat_lt (x : UInt64) :
x.toNat < 2 ^ 64
source
@[simp]
theorem UInt64.toUInt8_toNat (x : UInt64) :
x.toUInt8.toNat = x.toNat % 2 ^ 8
source
@[simp]
theorem UInt64.toUInt16_toNat (x : UInt64) :
x.toUInt16.toNat = x.toNat % 2 ^ 16
source
@[simp]
theorem UInt64.toUInt32_toNat (x : UInt64) :
x.toUInt32.toNat = x.toNat % 2 ^ 32
source
theorem UInt64.toNat_add (x : UInt64) (y : UInt64) :
(x + y).toNat = (x.toNat + y.toNat) % UInt64.size
source
theorem UInt64.toNat_sub (x : UInt64) (y : UInt64) :
(x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size
source
theorem UInt64.toNat_mul (x : UInt64) (y : UInt64) :
(x * y).toNat = x.toNat * y.toNat % UInt64.size
source
theorem UInt64.le_antisymm_iff {x : UInt64} {y : UInt64} :
x = y ↔ x ≤ y ∧ y ≤ x
source
theorem UInt64.le_antisymm {x : UInt64} {y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) :
x = y
source
instance instLawfulOrdUInt64 :
Batteries.LawfulOrd UInt64
Equations

USize #

source
theorem USize.ext {x : USize} {y : USize} :
x.toNat = y.toNat → x = y
source
@[simp]
theorem USize.val_val_eq_toNat (x : USize) :
↑x.val = x.toNat
source
@[simp]
theorem USize.toNat_ofNat (n : Nat) :
(OfNat.ofNat n).toNat = n % USize.size
source
theorem USize.size_eq :
USize.size = 2 ^ System.Platform.numBits
source
theorem USize.le_size :
2 ^ 32 ≤ USize.size
source
theorem USize.size_le :
USize.size ≤ 2 ^ 64
source
theorem USize.toNat_lt (x : USize) :
x.toNat < 2 ^ System.Platform.numBits
source
@[simp]
theorem USize.toUInt64_toNat (x : USize) :
x.toUInt64.toNat = x.toNat
source
@[simp]
theorem UInt32.toUSize_toNat (x : UInt32) :
x.toUSize.toNat = x.toNat
source
theorem USize.toNat_add (x : USize) (y : USize) :
(x + y).toNat = (x.toNat + y.toNat) % USize.size
source
theorem USize.toNat_sub (x : USize) (y : USize) :
(x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size
source
theorem USize.toNat_mul (x : USize) (y : USize) :
(x * y).toNat = x.toNat * y.toNat % USize.size
source
theorem USize.le_antisymm_iff {x : USize} {y : USize} :
x = y ↔ x ≤ y ∧ y ≤ x
source
theorem USize.le_antisymm {x : USize} {y : USize} (h1 : x ≤ y) (h2 : y ≤ x) :
x = y
source
instance instLawfulOrdUSize :
Batteries.LawfulOrd USize
Equations