diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 0bcca0fe56..4675fe3248 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -4847,7 +4847,7 @@ For instance, the following lemma: .. coqdoc:: - Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). + Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). relates the boolean conjunction to the logical one ``/\``. Note that in ``andP``, ``b1`` and ``b2`` are two boolean variables and the @@ -4901,7 +4901,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. coqtop:: none - Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). + Restart. .. coqtop:: all |