Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting


chronological Thread 
  • From: Stephane Glondu <steph AT glondu.net>
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting
  • Date: Fri, 15 Feb 2008 16:09:40 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Edsko de Vries a écrit :
which is reasonably nice (we should introduce some custom notation,
perhaps). It would be nicer if we should pass in a position, but
unfortunately if we define

Ltac rewrite_at t t' pos := let H := fresh in
    set (H := t) in |- * at pos ;
    rewrite t' ;
    subst H.

then
rewrite_at a ab 1.

gives

  User error: Ltac variable pos is bound to a term
    which cannot be coerced to an integer

What about:

Tactic Notation "rewrite_at" constr(t) constr(t') integer(pos) :=
    let H := fresh in
    set (H := t) in |- * at pos ;
    rewrite t' ;
    subst H.


Cheers,

--
Stéphane





Archive powered by MhonArc 2.6.16.

Top of Page