diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean
index 19c495abc7..265b3d1dcc 100644
--- a/src/Init/Data/OfScientific.lean
+++ b/src/Init/Data/OfScientific.lean
@@ -80,9 +80,9 @@ instance : OfScientific Float32 where
 def Float32.ofNat (n : Nat) : Float32 :=
   OfScientific.ofScientific n false 0
 
-def Float32.ofInt : Int → Float
-  | Int.ofNat n => Float.ofNat n
-  | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
+def Float32.ofInt : Int → Float32
+  | Int.ofNat n => Float32.ofNat n
+  | Int.negSucc n => Float32.neg (Float32.ofNat (Nat.succ n))
 
 instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
 
diff --git a/tests/lean/run/float32.lean b/tests/lean/run/float32.lean
index a70fbdcf88..d6fe2c3a01 100644
--- a/tests/lean/run/float32.lean
+++ b/tests/lean/run/float32.lean
@@ -36,3 +36,16 @@ info: 0.909297
 /-- info: 1606938044258990275541962092341162602522202993782792835301376.000000 -/
 #guard_msgs in
 #eval (2 : Float32).toFloat ^ (200 : Float32).toFloat
+
+#guard (Float32.ofInt (-1 : Int)).toBits == 0xBF800000
+
+-- 2^24 + 1 is the smallest Nat that can't be represented exactly in FP32 but can in FP64;
+-- There are 23 bits of mantissa and an implicit leading 1. Additionally, powers of
+-- 2 (within range) are exactly representable in either format.
+-- This shows that we are not accidentally representing Float32 with 64 bits;
+#guard
+  let n := Int.pow 2 24
+  (Float.ofInt n) - (Float32.ofInt n).toFloat == 0
+#guard
+  let n := Int.pow 2 24 + 1
+  (Float.ofInt n) - (Float32.ofInt n).toFloat != 0