coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Rewritinig *one* occurrence using setoid rewriting, Edsko de Vries
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Damien Pous
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Edsko de Vries
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting, Stephane Glondu
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Edsko de Vries
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting, Vincent Aravantinos
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting, Brian Aydemir
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Edsko de Vries
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting, Stephane Glondu
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Edsko de Vries
- Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting,
Damien Pous
Archive powered by MhonArc 2.6.16.