Std.Data.UInt

UInt8 #

source

theorem UInt8.ext {x : UInt8} {y : UInt8} :

x.toNat = y.toNat → x = y

source

theorem UInt8.ext_iff {x : UInt8} {y : UInt8} :

x = y ↔ x.toNat = y.toNat

source

@[simp]

theorem UInt8.val_val_eq_toNat (x : UInt8) :

↑x.val = x.toNat

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.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 :

Std.LawfulOrd UInt8

Equations

instLawfulOrdUInt8 = ⋯

UInt16 #

source

theorem UInt16.ext {x : UInt16} {y : UInt16} :

x.toNat = y.toNat → x = y

source

theorem UInt16.ext_iff {x : UInt16} {y : UInt16} :

x = y ↔ x.toNat = y.toNat

source

theorem UInt16.toNat_lt (x : UInt16) :

x.toNat < 2 ^ 16

source

@[simp]

theorem UInt16.val_val_eq_toNat (x : UInt16) :

↑x.val = x.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

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 :

Std.LawfulOrd UInt16

Equations

instLawfulOrdUInt16 = ⋯

UInt32 #

source

theorem UInt32.ext {x : UInt32} {y : UInt32} :

x.toNat = y.toNat → x = y

source

theorem UInt32.ext_iff {x : UInt32} {y : UInt32} :

x = y ↔ x.toNat = y.toNat

source

@[simp]

theorem UInt32.val_val_eq_toNat (x : UInt32) :

↑x.val = x.toNat

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.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 :

Std.LawfulOrd UInt32

Equations

instLawfulOrdUInt32 = ⋯

UInt64 #

source

theorem UInt64.ext {x : UInt64} {y : UInt64} :

x.toNat = y.toNat → x = y

source

theorem UInt64.ext_iff {x : UInt64} {y : UInt64} :

x = y ↔ x.toNat = y.toNat

source

@[simp]

theorem UInt64.val_val_eq_toNat (x : UInt64) :

↑x.val = x.toNat

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.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 :

Std.LawfulOrd UInt64

Equations

instLawfulOrdUInt64 = ⋯

USize #

source

theorem USize.ext {x : USize} {y : USize} :

x.toNat = y.toNat → x = y

source

theorem USize.ext_iff {x : USize} {y : USize} :

x = y ↔ x.toNat = y.toNat

source

@[simp]

theorem USize.val_val_eq_toNat (x : USize) :

↑x.val = x.toNat

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.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 :

Std.LawfulOrd USize

Equations

instLawfulOrdUSize = ⋯