coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jim Apple <coq-club AT jbapple.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] running out of memory with big proof objects
- Date: Tue, 19 Oct 2010 18:15:17 -0400
You might try "Proof Trick: Small Inversions"
http://hal.inria.fr/inria-00489412/en/
http://www-verimag.imag.fr/~monin/Proof/SmallInversion/small_inversions.v
On Tue, Oct 19, 2010 at 6:10 PM, Aaron Bohannon
<bohannon AT cis.upenn.edu>
wrote:
> It seems like something must be wrong here. Is there something I
> should be using instead of "inversion H; congruence"?
- [Coq-Club] running out of memory with big proof objects, Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Adam Chlipala
- Re: [Coq-Club] running out of memory with big proof objects, Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects, Jim Apple
- Message not available
- Message not available
- Fwd: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Stéphane Lescuyer
- Re: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects, Aaron Bohannon
- Message not available
- Re: [Coq-Club] running out of memory with big proof objects, Stéphane Lescuyer
- Re: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Stéphane Lescuyer
- Fwd: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Message not available
- Message not available
- Re: [Coq-Club] running out of memory with big proof objects,
Adam Chlipala
- Re: [Coq-Club] running out of memory with big proof objects, Stéphane Lescuyer
- [Coq-Club] Re: running out of memory with big proof objects, Adam Megacz
Archive powered by MhonArc 2.6.16.