max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix comment for Unit

Browse source
This commit is contained in:
Marcus Rossel 2023-09-05 07:36:23 +02:00 • committed by Sebastian Ullrich
parent 66e1472c7e
commit 84bf315ac8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Prelude.lean
View file

@ -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.