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

chore: rename IntX.toNat -> IntX.toNatClampNeg (#7066)

Browse source 
This PR renames `IntX.toNat` to `IntX.toNatClampNeg` (to reduce
surprises) and sets up a deprecation.
This commit is contained in:
Markus Himmel 2025-02-13 13:14:28 +01:00 • committed by GitHub
parent a3fd2eb0fe
commit 4a900cc65c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/Data/SInt/Basic.lean
View file

@ -93,7 +93,9 @@ def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
@[inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
@[inline, deprecated Int8.toNatClampNeg (since := "2025-02-13"), inherit_doc Int8.toNatClampNeg]
def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
/-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
@[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
@[extern "lean_int8_neg"]
@ -199,7 +201,9 @@ def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
@[inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
@[inline, deprecated Int16.toNatClampNeg (since := "2025-02-13"), inherit_doc Int16.toNatClampNeg]
def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
/-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
@[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
@[extern "lean_int16_to_int8"]
@ -309,7 +313,9 @@ def Int32.toInt (i : Int32) : Int := i.toBitVec.toInt
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
@[inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
@[inline, deprecated Int32.toNatClampNeg (since := "2025-02-13"), inherit_doc Int32.toNatClampNeg]
def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
/-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
@[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
@[extern "lean_int32_to_int8"]
@ -423,7 +429,9 @@ def Int64.toInt (i : Int64) : Int := i.toBitVec.toInt
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
@[inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
@[inline, deprecated Int64.toNatClampNeg (since := "2025-02-13"), inherit_doc Int64.toNatClampNeg]
def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
/-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
@[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
@[extern "lean_int64_to_int8"]
@ -541,7 +549,9 @@ def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
@[inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
@[inline, deprecated ISize.toNatClampNeg (since := "2025-02-13"), inherit_doc ISize.toNatClampNeg]
def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
/-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
@[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩
@[extern "lean_isize_to_int8"]