Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Erasable Red/Black Trees in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Erasable Red/Black Trees in Coq


Chronological Thread 
  • 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.
Proof.
  intros A p q r s H.
  rewrite H. (*fails*)

I guess the thing to do is to use the AACTactics library with ILists.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page