diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 6 |
2 files changed, 5 insertions, 5 deletions
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..98445fca1a 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -405,7 +405,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 +445,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 |