Documentation

Batteries.Data.UInt

UInt8 #

source
theorem UInt8.ext {x y : UInt8} :
x.toNat = y.toNat → x = y
source
theorem UInt8.ext_iff {x y : UInt8} :
x = y ↔ x.toNat = y.toNat
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
📐 coverage
instance instLawfulOrdUInt8 :
Std.LawfulOrd UInt8
source
theorem UInt8.le_iff_toNat_le_toNat {x y : UInt8} :
x ≤ y ↔ x.toNat ≤ y.toNat
source
theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} :
x < y ↔ x.toNat < y.toNat
source
theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) :
compare x y = compare x.toNat y.toNat
source
theorem UInt8.max_def (x y : UInt8) :
max x y = if x ≤ y then y else x
source
theorem UInt8.min_def (x y : UInt8) :
min x y = if x ≤ y then x else y
source
theorem UInt8.toNat_max (x y : UInt8) :
(max x y).toNat = max x.toNat y.toNat
source
theorem UInt8.toNat_min (x y : UInt8) :
(min x y).toNat = min x.toNat y.toNat

UInt16 #

source
theorem UInt16.ext {x y : UInt16} :
x.toNat = y.toNat → x = y
source
theorem UInt16.ext_iff {x y : UInt16} :
x = y ↔ x.toNat = y.toNat
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
📐 coverage
instance instLawfulOrdUInt16 :
Std.LawfulOrd UInt16
source
theorem UInt16.le_iff_toNat_le_toNat {x y : UInt16} :
x ≤ y ↔ x.toNat ≤ y.toNat
source
theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} :
x < y ↔ x.toNat < y.toNat
source
theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) :
compare x y = compare x.toNat y.toNat
source
theorem UInt16.max_def (x y : UInt16) :
max x y = if x ≤ y then y else x
source
theorem UInt16.min_def (x y : UInt16) :
min x y = if x ≤ y then x else y
source
theorem UInt16.toNat_max (x y : UInt16) :
(max x y).toNat = max x.toNat y.toNat
source
theorem UInt16.toNat_min (x y : UInt16) :
(min x y).toNat = min x.toNat y.toNat

UInt32 #

source
theorem UInt32.ext {x y : UInt32} :
x.toNat = y.toNat → x = y
source
theorem UInt32.ext_iff {x y : UInt32} :
x = y ↔ x.toNat = y.toNat
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
📐 coverage
instance instLawfulOrdUInt32 :
Std.LawfulOrd UInt32
source
theorem UInt32.le_iff_toNat_le_toNat {x y : UInt32} :
x ≤ y ↔ x.toNat ≤ y.toNat
source
theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} :
x < y ↔ x.toNat < y.toNat
source
theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) :
compare x y = compare x.toNat y.toNat
source
theorem UInt32.max_def (x y : UInt32) :
max x y = if x ≤ y then y else x
source
theorem UInt32.min_def (x y : UInt32) :
min x y = if x ≤ y then x else y
source
theorem UInt32.toNat_max (x y : UInt32) :
(max x y).toNat = max x.toNat y.toNat
source
theorem UInt32.toNat_min (x y : UInt32) :
(min x y).toNat = min x.toNat y.toNat

UInt64 #

source
theorem UInt64.ext {x y : UInt64} :
x.toNat = y.toNat → x = y
source
theorem UInt64.ext_iff {x y : UInt64} :
x = y ↔ x.toNat = y.toNat
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
📐 coverage
instance instLawfulOrdUInt64 :
Std.LawfulOrd UInt64
source
theorem UInt64.le_iff_toNat_le_toNat {x y : UInt64} :
x ≤ y ↔ x.toNat ≤ y.toNat
source
theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} :
x < y ↔ x.toNat < y.toNat
source
theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) :
compare x y = compare x.toNat y.toNat
source
theorem UInt64.max_def (x y : UInt64) :
max x y = if x ≤ y then y else x
source
theorem UInt64.min_def (x y : UInt64) :
min x y = if x ≤ y then x else y
source
theorem UInt64.toNat_max (x y : UInt64) :
(max x y).toNat = max x.toNat y.toNat
source
theorem UInt64.toNat_min (x y : UInt64) :
(min x y).toNat = min x.toNat y.toNat

USize #

source
theorem USize.ext {x y : USize} :
x.toNat = y.toNat → x = y
source
theorem USize.ext_iff {x y : USize} :
x = y ↔ x.toNat = y.toNat
source
theorem USize.toUInt64_toNat (x : USize) :
x.toUInt64.toNat = x.toNat
source
theorem UInt32.toUSize_toNat (x : UInt32) :
x.toUSize.toNat = x.toNat
source
📐 coverage
instance instLawfulOrdUSize :
Std.LawfulOrd USize
source
theorem USize.toNat_ofNat_of_le_of_lt {n i : Nat} (h : n < size) (hn : i ≤ n) :
(ofNat i).toNat = i
source
theorem USize.pred_toNat {i : USize} (h_gt : 0 < i) :
(i - 1).toNat = i.toNat - 1