From 031af730ae12601127d71b18adfc54d1a94eaaac Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 7 Jul 2020 10:14:44 +0200 Subject: [zify] Use flag for Z.to_euclidean_division_equations. Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross Co-authored-by: Jim Fehrle --- doc/sphinx/addendum/micromega.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/addendum') 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 `, 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 `, 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``. -- cgit v1.2.3