coq-club AT inria.fr

Subject: The Coq mailing list

List archive

The Hint command and rewriting rules.

From: "Laurent Reveillere [97-98]" <reveille AT labri.u-bordeaux.fr>
To: coq-club AT pauillac.inria.fr
Subject: The Hint command and rewriting rules.
Date: Thu, 05 Mar 1998 20:49:37 +0100
Organization: LaBRI, University of Bordeaux, FRANCE

Is there exist a means of adding a rewriting rule to the Hint list so
that the Auto command can thus make a series of simplification.

--
You can only find truth with logic
if you have already found truth without it.

The Hint command and rewriting rules., Laurent Reveillere [97-98]
- Re: The Hint command and rewriting rules., Micaela Mayero