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: Vincent Aravantinos <vincent.aravantinos AT gmail.com>
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: Stephane Glondu <steph AT glondu.net>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Rewritinig *one* occurrence using setoid rewriting
  • Date: Fri, 15 Feb 2008 16:30:36 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:subject:date:to:x-mailer:from; b=JGTqWWaQKNwVdYqjea1yVzyttv8JgjXNv75wg8whNFEvUwSVx1zdRXOBk0bWu1YXw4RpasOMRw8ZPvwc+UZAtyojlSk9RMDyA7NGwaSuW78ZVIeMZv+ZQZU0BD8BkLnlmHVfz0wLcwPrH9QYjqtJUHhhN07Mt2HbQd+zyqxqys4=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 15 févr. 08 à 16:26, Edsko de Vries a écrit :

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

Perfect! Thanks for that. Is that syntax (constr, integer) documented
anywhere? I can't find it in the chapter on tactics in the Coq manual.

It's in the chapter on notations : 11.4

V.



Archive powered by MhonArc 2.6.16.

Top of Page