From 935fcfb6ec84342163a86058856edcb1dca70ff4 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 25 Nov 2024 03:33:53 -0500
Subject: [PATCH] feat: non-opaque `UInt64.toUSize` (#6202)

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.
---
 src/Init/Data/UInt/Basic.lean | 3 +++
 src/Init/Prelude.lean         | 4 ----
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 263a9919ec..1c6b76acff 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -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⟩
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 35fd5c7ca4..5201230729 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -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`.