Documentation

Std.Data.UInt

UInt8 #

source
theorem UInt8.ext {x : UInt8} {y : UInt8} :
UInt8.toNat x = UInt8.toNat y → x = y
source
@[simp]
theorem UInt8.val_val_eq_toNat (x : UInt8) :
x.val.val = UInt8.toNat x
source
theorem UInt8.toNat_lt (x : UInt8) :
UInt8.toNat x < 2 ^ 8
source
@[simp]
theorem UInt8.toUInt16_toNat (x : UInt8) :
UInt16.toNat (UInt8.toUInt16 x) = UInt8.toNat x
source
@[simp]
theorem UInt8.toUInt32_toNat (x : UInt8) :
UInt32.toNat (UInt8.toUInt32 x) = UInt8.toNat x
source
@[simp]
theorem UInt8.toUInt64_toNat (x : UInt8) :
UInt64.toNat (UInt8.toUInt64 x) = UInt8.toNat x

UInt16 #

source
theorem UInt16.ext {x : UInt16} {y : UInt16} :
UInt16.toNat x = UInt16.toNat y → x = y
source
theorem UInt16.toNat_lt (x : UInt16) :
UInt16.toNat x < 2 ^ 16
source
@[simp]
theorem UInt16.val_val_eq_toNat (x : UInt16) :
x.val.val = UInt16.toNat x
source
@[simp]
theorem UInt16.toUInt8_toNat (x : UInt16) :
UInt8.toNat (UInt16.toUInt8 x) = UInt16.toNat x % 2 ^ 8
source
@[simp]
theorem UInt16.toUInt32_toNat (x : UInt16) :
UInt32.toNat (UInt16.toUInt32 x) = UInt16.toNat x
source
@[simp]
theorem UInt16.toUInt64_toNat (x : UInt16) :
UInt64.toNat (UInt16.toUInt64 x) = UInt16.toNat x

UInt32 #

source
theorem UInt32.ext {x : UInt32} {y : UInt32} :
UInt32.toNat x = UInt32.toNat y → x = y
source
@[simp]
theorem UInt32.val_val_eq_toNat (x : UInt32) :
x.val.val = UInt32.toNat x
source
theorem UInt32.toNat_lt (x : UInt32) :
UInt32.toNat x < 2 ^ 32
source
@[simp]
theorem UInt32.toUInt8_toNat (x : UInt32) :
UInt8.toNat (UInt32.toUInt8 x) = UInt32.toNat x % 2 ^ 8
source
@[simp]
theorem UInt32.toUInt16_toNat (x : UInt32) :
UInt16.toNat (UInt32.toUInt16 x) = UInt32.toNat x % 2 ^ 16
source
@[simp]
theorem UInt32.toUInt64_toNat (x : UInt32) :
UInt64.toNat (UInt32.toUInt64 x) = UInt32.toNat x

UInt64 #

source
theorem UInt64.ext {x : UInt64} {y : UInt64} :
UInt64.toNat x = UInt64.toNat y → x = y
source
@[simp]
theorem UInt64.val_val_eq_toNat (x : UInt64) :
x.val.val = UInt64.toNat x
source
theorem UInt64.toNat_lt (x : UInt64) :
UInt64.toNat x < 2 ^ 64
source
@[simp]
theorem UInt64.toUInt8_toNat (x : UInt64) :
UInt8.toNat (UInt64.toUInt8 x) = UInt64.toNat x % 2 ^ 8
source
@[simp]
theorem UInt64.toUInt16_toNat (x : UInt64) :
UInt16.toNat (UInt64.toUInt16 x) = UInt64.toNat x % 2 ^ 16
source
@[simp]
theorem UInt64.toUInt32_toNat (x : UInt64) :
UInt32.toNat (UInt64.toUInt32 x) = UInt64.toNat x % 2 ^ 32

USize #

source
theorem USize.ext {x : USize} {y : USize} :
USize.toNat x = USize.toNat y → x = y
source
@[simp]
theorem USize.val_val_eq_toNat (x : USize) :
x.val.val = USize.toNat x
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) :
USize.toNat x < 2 ^ System.Platform.numBits
source
@[simp]
theorem USize.toUInt64_toNat (x : USize) :
UInt64.toNat (USize.toUInt64 x) = USize.toNat x
source
@[simp]
theorem UInt32.toUSize_toNat (x : UInt32) :
USize.toNat (UInt32.toUSize x) = UInt32.toNat x