max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: non-opaque UInt64.toUSize (#6202)

Browse source 
This PR makes `USize.toUInt64` a regular non-opaque definition. 

It also moves it to `Init.Data.UInt.Basic`, as it is not actually used
in `Init.Prelude` anymore.
This commit is contained in:
Mac Malone 2024-11-25 03:33:53 -05:00 • committed by GitHub
parent 20acc72a29
commit 935fcfb6ec
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/UInt/Basic.lean
View file

@ -268,6 +268,9 @@ def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.of
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
@[extern "lean_usize_to_uint32"]
def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
/-- Converts a `UInt64` to a `USize` by reducing modulo `USize.size`. -/
@[extern "lean_uint64_to_usize"]
def UInt64.toUSize (a : UInt64) : USize := a.toNat.toUSize
instance : Mul USize := ⟨USize.mul⟩
instance : Mod USize := ⟨USize.mod⟩

4
src/Init/Prelude.lean
View file

@ -3432,10 +3432,6 @@ class Hashable (α : Sort u) where
export Hashable (hash)
/-- Converts a `UInt64` to a `USize` by reducing modulo `USize.size`. -/
@[extern "lean_uint64_to_usize"]
opaque UInt64.toUSize (u : UInt64) : USize
/--
Upcast a `USize` to a `UInt64`.
This is lossless because `USize.size` is either `2^32` or `2^64`.