coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 |
- [Coq-Club] suggestion, Jean-Yves Vion-Dury
Archive powered by MhonArc 2.6.16.