The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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