diff options
| author | Enrico Tassi | 2019-01-24 14:33:01 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-24 14:33:01 +0100 |
| commit | fddca21344c6f72f7442f2a44fd46212b11ac521 (patch) | |
| tree | b458f809ff9231995d857071cf9386ef884652a9 | |
| parent | 5cf39fac26282b63b2c90663ef0be3c4e7b051ff (diff) | |
[doc] explain how to avoid automatic clears
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index d7aa0e1b07..8c1ca036cb 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1604,6 +1604,9 @@ A :token:`clear_switch` that immediately precedes an :token:`i_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}``. +This behavior can be avoided by separating the :token:`clear_switch` +from the :token:`i_view` with the ``-`` intro pattern or by putting +parentheses around the view. A :token:`clear_switch` that immediately precedes an :token:`i_view` is executed after the view application. @@ -1637,6 +1640,8 @@ Intro patterns is a simple proof context entry [#10]_. As a consequence by prefixing the :token:`ident` with ``{}`` one can *replace* a context entry. + This behavior can be avoided by separating the :token:`clear_switch` + from the :token:`ident` with the ``-`` intro pattern. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur @@ -3076,6 +3081,7 @@ operation should be performed: As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. + This behavior can be avoided by putting parentheses around the rewrite rule. An :token:`r_item` can be: |