coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] autorewrite for hypothesis?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: Eric Mullen <emullen AT cs.washington.edu>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] autorewrite for hypothesis?
Date: Thu, 14 Nov 2013 09:08:52 +0000
Accept-language: de-DE, en-US

Dear Eric,

thanks for pointing me to this useful tactic! But in this specific case the terms (f true) and (f false) are replaced recursively in expressions like f (f (f true)) and subst only works on identifiers, so it is not applicable here.

Best regards,

Michael

From: Eric Mullen
Sent: Wednesday, November 13, 2013 8:30 PM

How about subst? Have you tried that tactic?

Best!

Eric

Re: [Coq-Club] Posting my first bigger stuff (for experience/training), (continued)