diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4fc3c24e89..bcef988874 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -4935,9 +4935,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4947,12 +4947,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but |