From dd293d1fbda7b8695875f435ca78d58a3e4f7278 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 8 Feb 2025 10:11:26 -0800 Subject: [PATCH] doc: mention `Prop`s are equal to `True` or `False` (#6998) 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. --- src/Lean/Parser/Term.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index c1510a4ed9..ce582bbb3f 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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" /--