From 4262ea14d60517a51a5fb9957140fabe4734f479 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 13 Mar 2025 07:24:42 +0100
Subject: [PATCH] fix: `Repr` instance for `Int32` (#7467)

This PR fixes the `Repr Int32` instance, which was previously repeating
the `Repr Int16` instance due to a copy-and-paste error.
---
 src/Init/Data/SInt/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 88521af4f4..5f1975468e 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -402,9 +402,9 @@ def Int32.neg (i : Int32) : Int32 := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString Int32 where
   toString i := toString i.toInt
-instance : Repr Int16 where
+instance : Repr Int32 where
   reprPrec i prec := reprPrec i.toInt prec
-instance : ReprAtom Int16 := ⟨⟩
+instance : ReprAtom Int32 := ⟨⟩
 
 instance : Hashable Int32 where
   hash i := i.toUInt32.toUInt64