From a26c937650ebdcfe7f33a54e0906092bc8e4e767 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Tue, 18 Feb 2025 12:03:53 +0100
Subject: [PATCH] feat: `Repr` and `Hashable` for `IntX` (#7128)

This PR adds `Repr` and `Hashable` instances for `IntX`.
---
 src/Init/Data/SInt/Basic.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 6814f487f4..f7ab8badf5 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -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