coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: The Hint command and rewriting rules.

From: Micaela Mayero <mayero AT bouzy.inria.fr>
To: reveille AT labri.u-bordeaux.fr (Laurent Reveillere [97-98])
Cc: coq-club AT pauillac.inria.fr
Subject: Re: The Hint command and rewriting rules.
Date: Thu, 19 Mar 1998 19:04:15 +0100 (MET)

> 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.
>

This possibility has not been implemented for it would be applied to all the
goals and it would slow Auto too much.

Regards,

Micaela Mayero.

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