diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ae721c2430..d7aa0e1b07 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1601,10 +1601,14 @@ It interprets the top of the stack with the view :token:`term`. It is equivalent to :n:`move/@term`. A :token:`clear_switch` that immediately precedes an :token:`i_view` -that happen to be a :token:`ident` is extended with that -:token:`ident` and the :token:`clear_switch` is executed after the view. +is complemented with the name of the view whenever the :token:`i_view` +is a simple proof context entry [#10]_. E.g. ``{}/v`` is equivalent to ``/v{v}``. +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is executed after the view application. + + If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. @@ -1629,8 +1633,9 @@ Intro patterns Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. A :token:`clear_switch` (even an empty one) immediately preceding an - :token:`ident` is extended with that :token:`ident` if the identifier - points to an existing context entry. As a consequence by prefixing the + :token:`ident` is complemented with that :token:`ident` if the identifier + is a simple proof context entry [#10]_. + As a consequence by prefixing the :token:`ident` with ``{}`` one can *replace* a context entry. ``>`` pops every variable occurring in the rest of the stack. @@ -3067,7 +3072,8 @@ operation should be performed: A clear switch, even an empty one, is performed *after* the :token:`r_item` is actually processed and is complemented with the name of - the rewrite rule when it is a simple context entry. As a consequence one can + the rewrite rule when it is a simple proof context entry [#10]_. + As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. @@ -5549,3 +5555,5 @@ Settings in the metatheory .. [#9] The current state of the proof shall be displayed by the Show Proof command of |Coq| proof mode. +.. [#10] A simple proof context entry is a naked identifier (i.e. not between + parentheses) designating a context entry that is not a section variable. |