Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to make ring_nat available

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to make ring_nat available


chronological Thread 
  • From: "St�phane Lescuyer" <lescuyer AT lri.fr>
  • To: Cedric.Auger AT lri.fr
  • Cc: "Yves Bertot" <Yves.Bertot AT sophia.inria.fr>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] how to make ring_nat available
  • Date: Wed, 22 Oct 2008 17:08:04 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=SBIJ0TKw1PhM0T1NnDn+l9qWqr7kZBy6UIhYRox4S4tr/2GeJIqREQFLiwVjGg9QRG UVyt7xPxgBxWkOYS0hCJkgiyH+a8Zb7QejdCkTq0ibWj0H+z51QAq4viuRQ1XTrl+p97 fCB0srlPOIUMiiOm56VI8LtrI+I1R//FDnFj8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Wed, Oct 22, 2008 at 4:33 PM, AUGER Cédric 
<Cedric.Auger AT lri.fr>
 wrote:
> I have never used tactic ring, but why using such a name while (nat, 0, +,
> *) is not a ring?

Because the tactic ring can deal both with rings (Z, Q, ...) and
semi-rings (bool, nat, ...): it essentially does AC rewriting in order
to normalize polynomial expressions. Of course, it only takes the
opposite operation into account when you're in a ring and not a
semi-ring. Finally, 'ring' is shorter to type than 'semiring' :-)

SL



Archive powered by MhonArc 2.6.16.

Top of Page