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

doc: mention Props are equal to True or False (#6998)

Browse source 
This PR modifies the `Prop` docstring to point out that every
proposition is propositionally equal to either `True` or `False`. This
will help point users toward seeing that `Prop` is like `Bool`.

I considered mentioning `Classical.propComplete`, but it's probably
better not making it seem like that's how you should work with
propositions.
This commit is contained in:
Kyle Miller 2025-02-08 10:11:26 -08:00 • committed by GitHub
parent 4989a60af3
commit dd293d1fbd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Term.lean
View file

@ -138,7 +138,9 @@ def optSemicolon (p : Parser) : Parser :=
/-- A specific universe in Lean's infinite hierarchy of universes. -/
@[builtin_term_parser] def sort := leading_parser
"Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
/-- The universe of propositions. `Prop ≡ Sort 0`. -/
/-- The universe of propositions. `Prop ≡ Sort 0`.
Every proposition is propositionally equal to either `True` or `False`. -/
@[builtin_term_parser] def prop := leading_parser
"Prop"
/--