diff options
| author | coqbot-app[bot] | 2020-11-20 15:30:35 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 15:30:35 +0000 |
| commit | 1aca82b3d8ff562b75a5a93a5910afd39c10ba3b (patch) | |
| tree | 365297142cd0a002495301b770f8d266c9a68575 | |
| parent | dac6017513cea37f96ce8256239e490f18339f08 (diff) | |
| parent | fe56bc97653123d24631b0f9ed2e100259202099 (diff) | |
Merge PR #13426: [doc] [ssr] fix documentation of reflect
Reviewed-by: CohenCyril
| -rw-r--r-- | theories/ssr/ssrbool.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index b205965ed1..d1cefeb552 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -22,9 +22,10 @@ Require Import ssreflect ssrfun. is_true b == the coercion of b : bool to Prop (:= b = true). This is just input and displayed as `b''. reflect P b == the reflection inductive predicate, asserting - that the logical proposition P : prop with the - formula b : bool. Lemmas asserting reflect P b - are often referred to as "views". + that the logical proposition P : Prop holds iff + the formula b : bool is equal to true. Lemmas + asserting reflect P b are often referred to as + "views". iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection views: iffP is used to prove reflection from logical equivalence, appP to compose views, and @@ -33,7 +34,7 @@ Require Import ssreflect ssrfun. elimT :: coercion reflect >-> Funclass, which allows the direct application of `reflect' views to boolean assertions. - decidable P <-> P is effectively decidable (:= {P} + {~ P}. + decidable P <-> P is effectively decidable (:= {P} + {~ P}). contra, contraL, ... :: contraposition lemmas. altP my_viewP :: natural alternative for reflection; given lemma myviewP: reflect my_Prop my_formula, |