coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Erasable Red/Black Trees in Coq
- Date: Fri, 25 Apr 2014 23:24:02 -0400
Arnaud, I somewhat expected to get associative rewriting of ILists as well - but that isn't working: Remark assoc_rw : forall A (p q r s:IList A), q++r = s -> (p++q)++r = p++s. I guess the thing to do is to use the AACTactics library with ILists. -- Jonathan |
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, (continued)
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/28/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jason Gross, 04/28/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Cedric Auger, 04/28/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
Archive powered by MHonArc 2.6.18.