diff options
| author | Enrico Tassi | 2020-11-20 10:14:21 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-20 10:14:21 +0100 |
| commit | fe56bc97653123d24631b0f9ed2e100259202099 (patch) | |
| tree | 0eca6d23b91d697566533287f58ccf782c552072 | |
| parent | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (diff) | |
[doc] [ssr] fix documentation of reflect
| -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, |