diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-16 11:16:47 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-05 14:41:54 +0200 |
commit | efd0d33dac811c06412926445e28c2158f7ee1d3 (patch) | |
tree | 8381df41c35e3c69fd67965cdcad242e95fadc92 /doc/sphinx/proof-engine/ssreflect-proof-language.rst | |
parent | 0e48f50f2c84bafc410097bd67fab66b10947bf3 (diff) |
[ssr] index entry for "without loss", "suffices" and "generally have"
Diffstat (limited to 'doc/sphinx/proof-engine/ssreflect-proof-language.rst')
-rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index f842c6e31..1a48d44b3 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2832,6 +2832,7 @@ should be generalized. The general syntax of without loss is: .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term :name: wlog +.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term where each :token:`ident` is a constant in the context of the goal. Open syntax is supported for :token:`term`. @@ -2839,6 +2840,7 @@ of the goal. Open syntax is supported for :token:`term`. In its defective form: .. tacv:: wlog: / @term +.. tacv:: without loss: / @term on a goal G, it creates two subgoals: a first one to prove the @@ -5391,6 +5393,7 @@ rewrite see :ref:`rewriting_ssr` .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } +.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } forward chaining see :ref:`structure_ssr` @@ -5400,7 +5403,9 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` .. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } +.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } backchaining see :ref:`structure_ssr` |