Skip to Content.
Sympa Menu

coq-club - [Coq-Club] suggestion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] suggestion


chronological Thread 
  • From: Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] suggestion
  • Date: Thu, 13 Nov 2003 15:37:22 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Organization: Inria Rhones-Alpes

Dear all,

Writing my own tactics, I often need an abstraction that could be quite useful: automatic fresh label generation.
The idea could be to use a particular notation, such as #id, in order to ask for a fresh name w.r.t the current context.

Intro generates fresh labels, but one cannot explicitely refer to them...

e.g. :

        Match Context With [ id: {?=true}+{?=false} |- ? ] -> Elim id;Intros #H;Rewrite #H;...

J.-Yves

N.B. Perhaps it is possible to do this by using existing primitives, but I can't figure out how to do it...


--
Jean-Yves Vion-Dury   Research Scientist     Xerox Research Centre Europe
INRIA (sabbatical)
655 avenue de l'Europe,
38334 Montbonnot (FRANCE)
Jean-Yves.Vion-Dury AT inrialpes.fr
from France:   0 4 76 61 53 83
from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language? www.alphaAve.com



Archive powered by MhonArc 2.6.16.

Top of Page