diff options
| author | Frédéric Besson | 2020-07-07 10:14:44 +0200 |
|---|---|---|
| committer | BESSON Frederic | 2020-10-20 10:02:19 +0200 |
| commit | 031af730ae12601127d71b18adfc54d1a94eaaac (patch) | |
| tree | 97443f67a20600c6e5688fd2a1a36ca4d05b25ca /doc | |
| parent | a2f5cc26baca0db087a677196f186ac2f75aa484 (diff) | |
[zify] Use flag for Z.to_euclidean_division_equations.
Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 01aed122b2..b3a33ffeea 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -283,8 +283,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. tacn:: zify :name: zify - This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. - Some additional support is provided by the following modules + This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. + Additional support is provided by the following modules: + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`. + For comparison operators (e.g., :g:`Z.compare`), require the module :g:`ZifyComparison`. @@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. - + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. |