Documentation

Batteries.Data.UInt

UInt8 #

source
theorem UInt8.ext {x y : UInt8} :
x.toNat = y.toNat → x = y
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
instance instLawfulOrdUInt8 :
Batteries.LawfulOrd UInt8

UInt16 #

source
theorem UInt16.ext {x y : UInt16} :
x.toNat = y.toNat → x = y
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
instance instLawfulOrdUInt16 :
Batteries.LawfulOrd UInt16

UInt32 #

source
theorem UInt32.ext {x y : UInt32} :
x.toNat = y.toNat → x = y
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
instance instLawfulOrdUInt32 :
Batteries.LawfulOrd UInt32

UInt64 #

source
theorem UInt64.ext {x y : UInt64} :
x.toNat = y.toNat → x = y
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
instance instLawfulOrdUInt64 :
Batteries.LawfulOrd UInt64

USize #

source
theorem USize.ext {x y : USize} :
x.toNat = y.toNat → x = y
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
instance instLawfulOrdUSize :
Batteries.LawfulOrd USize