diff options
| author | Théo Zimmermann | 2020-05-14 11:45:16 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 12:39:36 +0200 |
| commit | 95c4fc791b1eda5357855f706dfdb4c050d6c28e (patch) | |
| tree | df2e9f3316514b01f2f84a53f5ea882d310c1188 /doc/sphinx/proof-engine/tactics.rst | |
| parent | 6a9486eaa9a0de2af2f518cef09db7ea9afa9ab1 (diff) | |
Reintroduce leftover parts; update index files; small fixes.
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 127e4c6dbe..b660961279 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2977,6 +2977,41 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Performing computations --------------------------- +.. insertprodn red_expr pattern_occ + +.. prodn:: + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @smart_qualid } ] + strategy_flag ::= {+ @red_flags } + | @delta_flag + red_flags ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @num | @ident } } + | - {| @num | @ident } {* @int_or_var } + int_or_var ::= @int + | @ident + unfold_occ ::= @smart_qualid {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + This set of tactics implements different specialized usages of the tactic :tacn:`change`. |