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

feat: UIntX.ofFin (#7056)

Browse source 
This PR adds the `UIntX.ofFin` conversion functions.
This commit is contained in:
Markus Himmel 2025-02-13 09:45:01 +01:00 • committed by GitHub
parent 1ecb4a43ae
commit 7c9454edd2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -9,6 +9,8 @@ import Init.Data.BitVec.Basic
open Nat
/-- Converts a `Fin UInt8.size` into the corresponding `UInt8`. -/
@[inline] def UInt8.ofFin (a : Fin UInt8.size) : UInt8 := ⟨⟨a⟩⟩
@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
UInt8.ofBitVec bitVec
@ -76,6 +78,8 @@ instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
instance : Max UInt8 := maxOfLe
instance : Min UInt8 := minOfLe
/-- Converts a `Fin UInt16.size` into the corresponding `UInt16`. -/
@[inline] def UInt16.ofFin (a : Fin UInt16.size) : UInt16 := ⟨⟨a⟩⟩
@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
UInt16.ofBitVec bitVec
@ -145,6 +149,8 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
instance : Max UInt16 := maxOfLe
instance : Min UInt16 := minOfLe
/-- Converts a `Fin UInt32.size` into the corresponding `UInt32`. -/
@[inline] def UInt32.ofFin (a : Fin UInt32.size) : UInt32 := ⟨⟨a⟩⟩
@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
UInt32.ofBitVec bitVec
@ -199,6 +205,8 @@ instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
@[extern "lean_bool_to_uint32"]
def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
/-- Converts a `Fin UInt64.size` into the corresponding `UInt64`. -/
@[inline] def UInt64.ofFin (a : Fin UInt64.size) : UInt64 := ⟨⟨a⟩⟩
@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
UInt64.ofBitVec bitVec
@ -266,6 +274,8 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
instance : Max UInt64 := maxOfLe
instance : Min UInt64 := minOfLe
/-- Converts a `Fin USize.size` into the corresponding `USize`. -/
@[inline] def USize.ofFin (a : Fin USize.size) : USize := ⟨⟨a⟩⟩
@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
USize.ofBitVec bitVec

7
tests/lean/run/trivial_uint.lean
View file

@ -13,3 +13,10 @@ example : UInt16.ofBitVec 42 = 42 := by simp
example : UInt32.ofBitVec 42 = 42 := by simp
example : UInt64.ofBitVec 42 = 42 := by simp
example : USize.ofBitVec 42 = 42 := by simp
-- TODO: turn into `by simp` when the relevant theory is in place
example : UInt8.ofFin 42 = 42 := rfl
example : UInt16.ofFin 42 = 42 := rfl
example : UInt32.ofFin 42 = 42 := rfl
example : UInt64.ofFin 42 = 42 := rfl
example : USize.ofFin 42 = 42 := rfl