feat: Repr and Hashable for IntX (#7128)

This PR adds `Repr` and `Hashable` instances for `IntX`.
This commit is contained in:
Markus Himmel 2025-02-18 12:03:53 +01:00 committed by GitHub
parent 0929cb3902
commit a26c937650
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -103,6 +103,12 @@ def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
instance : ToString Int8 where
toString i := toString i.toInt
instance : Repr Int8 where
reprPrec i prec := reprPrec i.toInt prec
instance : ReprAtom Int8 := ⟨⟩
instance : Hashable Int8 where
hash i := i.toUInt8.toUInt64
instance : OfNat Int8 n := ⟨Int8.ofNat n⟩
instance : Neg Int8 where
@ -233,6 +239,12 @@ def Int16.neg (i : Int16) : Int16 := ⟨⟨-i.toBitVec⟩⟩
instance : ToString Int16 where
toString i := toString i.toInt
instance : Repr Int16 where
reprPrec i prec := reprPrec i.toInt prec
instance : ReprAtom Int16 := ⟨⟩
instance : Hashable Int16 where
hash i := i.toUInt16.toUInt64
instance : OfNat Int16 n := ⟨Int16.ofNat n⟩
instance : Neg Int16 where
@ -367,6 +379,12 @@ def Int32.neg (i : Int32) : Int32 := ⟨⟨-i.toBitVec⟩⟩
instance : ToString Int32 where
toString i := toString i.toInt
instance : Repr Int16 where
reprPrec i prec := reprPrec i.toInt prec
instance : ReprAtom Int16 := ⟨⟩
instance : Hashable Int32 where
hash i := i.toUInt32.toUInt64
instance : OfNat Int32 n := ⟨Int32.ofNat n⟩
instance : Neg Int32 where
@ -505,6 +523,12 @@ def Int64.neg (i : Int64) : Int64 := ⟨⟨-i.toBitVec⟩⟩
instance : ToString Int64 where
toString i := toString i.toInt
instance : Repr Int64 where
reprPrec i prec := reprPrec i.toInt prec
instance : ReprAtom Int64 := ⟨⟩
instance : Hashable Int64 where
hash i := i.toUInt64
instance : OfNat Int64 n := ⟨Int64.ofNat n⟩
instance : Neg Int64 where
@ -653,6 +677,12 @@ def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
instance : ToString ISize where
toString i := toString i.toInt
instance : Repr ISize where
reprPrec i prec := reprPrec i.toInt prec
instance : ReprAtom ISize := ⟨⟩
instance : Hashable ISize where
hash i := i.toUSize.toUInt64
instance : OfNat ISize n := ⟨ISize.ofNat n⟩
instance : Neg ISize where