coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unfold causes out of memory

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] unfold causes out of memory
Date: Fri, 12 Jul 2013 12:23:27 +0200

On Fri, Jul 12, 2013 at 12:18:02AM -0400, Abhishek Anand wrote:
> In my proofs, I only want to unfold it exactly once. Is there some way to
> do it.

You can (trivially) prove a lemma that states the unfolding equation,
and rewrite with it. Or better write a lemma for each reduction you
want to perform in a controlled way.

Cheers
--
Enrico Tassi

[Coq-Club] unfold causes out of memory, Abhishek Anand, 07/12/2013
- Re: [Coq-Club] unfold causes out of memory, Enrico Tassi, 07/12/2013