From 84bf315ac89be67b13913fdb7a42c9e859a7638b Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 5 Sep 2023 07:36:23 +0200
Subject: [PATCH] doc: fix comment for `Unit`

---
 src/Init/Prelude.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 4e2c2b9f8e..68fec587bf 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -116,7 +116,7 @@ In other words, it describes only a single value, which consists of said constru
 to no arguments whatsoever.
 The `Unit` type is similar to `void` in languages derived from C.
 
-`Unit` is actually defined as `PUnit.{0}` where `PUnit` is the universe
+`Unit` is actually defined as `PUnit.{1}` where `PUnit` is the universe
 polymorphic version. The `Unit` should be preferred over `PUnit` where possible to avoid
 unnecessary universe parameters.