diff options
| author | Théo Zimmermann | 2019-02-16 14:57:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:23:54 +0100 |
| commit | eb20b899a6cd0e3b9816a4b6824998255c4af6b8 (patch) | |
| tree | f48bbbd4dd03e6271d4a9a2c4ab47ad269517f76 /doc/sphinx/proof-engine | |
| parent | 6e09823bf1e2a93f2d726e6b100322740a5d52e7 (diff) | |
Fix last nested lemma failure.
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 |