The Coq mailing list

["julien.narboux" <julien.narboux AT laposte.net>]

Dear Jean-Yves, 
 
This is already implemented in the CVS version of Coq,  
The syntax is : "Let t = FreshId In" 
 
Here is an example : 
 
Welcome to Coq 8.0alpha (V7 syntax) (Sep 2003) 
 
Coq < Goal (A:Prop) A-> A. 
1 subgoal 
 
  ============================ 
   (A:Prop)A ->A 
 
Unnamed_thm < Let HCol = FreshId In Intro HCol. 
1 subgoal 
 
  H : Prop 
  ============================ 
   H ->H 
 
 
 
Julien Narboux 
 
 
 
 
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  
<http://www.xrce.xerox.com/people/vion-dury/home.html>   /Research  
Scientist/     * Xerox Research Centre Europe * 
*INRIA* (sabbatical) 
655 avenue de l'Europe, 
38334 Montbonnot (FRANCE) 
Jean-Yves.Vion-Dury AT inrialpes.fr
  
<mailto: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 <http://www.alphaAve.com> 

Accédez au courrier électronique de La Poste : www.laposte.net ; 
3615 LAPOSTENET (0,34€/mn) ; tél : 08 92 68 13 50 (0,34€/mn)