diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 |
4 files changed, 20 insertions, 16 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 27ae7cea3a..039a23e8c2 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -535,11 +535,19 @@ pass additional arguments such as ``using relation``. .. tacn:: setoid_reflexivity setoid_symmetry {? in @ident } setoid_transitivity @one_term - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident } - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @rewrite_occs } {? in @ident } + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @rewrite_occs setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 } :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace + .. todo: move rewrite_occs to rewrite chapter when that chapter is revised + + .. insertprodn rewrite_occs rewrite_occs + + .. prodn:: + rewrite_occs ::= {+ @integer } + | @ident + The ``using relation`` arguments cannot be passed to the unprefixed form. The latter argument tells the tactic what parametric relation should be used to replace the first tactic argument with the second one. If @@ -714,6 +722,8 @@ instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command :cmd:`Typeclasses Opaque`. +.. _strategies4rewriting: + Strategies for rewriting ------------------------ diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index fb9965e43a..28b60878d2 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -250,11 +250,11 @@ proof by abstracting monomials by variables. `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- -.. tacn:: psatz @one_term {? @int_or_var } +.. tacn:: psatz @one_term {? @nat_or_var } :name: psatz This tactic explores the *Cone* by increasing degrees – hence the - depth parameter *n*. In theory, such a proof search is complete – if the + depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the goal is provable the search eventually stops. Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a refutation. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 22527dc379..4143d836c4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -335,12 +335,6 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info one_pattern - - .. prodn:: - hint_info ::= %| {? @natural } {? @one_pattern } - one_pattern ::= @one_term - Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of @@ -405,7 +399,7 @@ Summary of the commands Shows the list of instances associated with the typeclass :token:`reference`. -.. tacn:: typeclasses eauto {? bfs } {? @int_or_var } {? with {+ @ident } } +.. tacn:: typeclasses eauto {? bfs } {? @nat_or_var } {? with {+ @ident } } This proof search tactic uses the resolution engine that is run implicitly during type checking. This tactic uses a different resolution @@ -445,11 +439,11 @@ Summary of the commands + Use the :cmd:`Typeclasses eauto` command to customize the behavior of this tactic. - :n:`@int_or_var` + :n:`@nat_or_var` Specifies the maximum depth of the search. .. warning:: - The semantics for the limit :n:`@int_or_var` + The semantics for the limit :n:`@nat_or_var` are different than for :tacn:`auto`. By default, if no limit is given, the search is unbounded. Unlike :tacn:`auto`, introduction steps count against the limit, which might result in larger limits being necessary when @@ -503,7 +497,7 @@ Typeclasses Transparent, Typeclasses Opaque It is useful when some constants prevent some unifications and make resolution fail. It is also useful to declare constants which - should never be unfolded during proof-search, like fixpoints or + should never be unfolded during proof search, like fixpoints or anything which does not look like an abbreviation. This can additionally speed up proof search as the typeclass map can be indexed by such rigid constants (see @@ -555,7 +549,7 @@ Settings This can be expensive as it requires rebuilding hint clauses dynamically, and does not benefit from the invertibility status of the product introduction rule, resulting in potentially more - expensive proof-search (i.e. more useless backtracking). + expensive proof search (i.e. more useless backtracking). .. flag:: Typeclass Resolution For Conversion diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 4615a8dfca..bb78b142ca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} - cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names |