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

doc: fix a typo in ULift's documentation (#8571)

Browse source 
Just a typo. From my understanding (and the specification otherwise) the
resulting level is the maximum of `r` and `s` instead of the minimum.

No issue opened yet (thus the draft).
This commit is contained in:
user202729 2025-06-01 13:25:52 +07:00 • committed by GitHub
parent bb6d1e000b
commit c6cad5fcff
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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

@ -861,7 +861,7 @@ instance : Inhabited NonemptyType.{u} where
Lifts a type to a higher universe level.
`ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be
the minimal level, it takes a further level parameter and occupies their minimum. The resulting type
the minimal level, it takes a further level parameter and occupies their maximum. The resulting type
may occupy any universe that's at least as large as that of `α`.
The resulting universe of the lifting operator is the first parameter, and may be written explicitly