Fix a typo in Prelude.lean

leanprover · Mar 13, 2024 · 2739e06 · 2739e06
1 parent 5aca09a
commit 2739e06
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
@@ -2035,7 +2035,7 @@ instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
 /--
-The size of type `UInt16`, that is, `2^System.Platform.numBits`, which may
+The size of type `USize`, that is, `2^System.Platform.numBits`, which may
 be either `2^32` or `2^64` depending on the platform's architecture.
 
 Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the