From 4ad36b5e2369b37aa2483a1e04eb628d147d97d3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 19 Aug 2020 13:07:14 -0400 Subject: Require NsatzTactic: nsatz support for Z and Q The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860 --- doc/sphinx/addendum/nsatz.rst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ed2e1ea58c..ed93145622 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -34,6 +34,12 @@ Nsatz: tactics for proving equalities in integral domains You can load the ``Nsatz`` module with the command ``Require Import Nsatz``. + Alternatively, if you prefer not to transitively depend on the + files declaring the axioms used to define the real numbers, you can + ``Require Import NsatzTactic`` instead; this will still allow + :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`, + :math:`\mathbb{Q}` and any user-registered rings. + More about `nsatz` --------------------- @@ -85,4 +91,4 @@ performed using :ref:`typeclasses`. then `lvar` is replaced by all the variables which are not in `parameters`. -See the file `Nsatz.v` for many examples, especially in geometry. +See the test-suite file `Nsatz.v `_ for many examples, especially in geometry. -- cgit v1.2.3