Re: [isabelle] Generating fresh type variables



Hi Mathieu,

There is also the related function Variable.variant_frees,
which is explained in the Cookbook on page 16 with a
small example about generating fresh names for Frees. ;o)

Hope this helps,
Christian


Sascha Boehme writes:
 > Hi Mathieu,
 > 
 > Concerning fresh names relative to a context have a look at the Isar
 > implementation manual in Chapter 5, Section 1 (Variables), especially
 > Variable.variant_fixes.  For more details, look into
 > ~~/src/Pure/variable.ML.
 > 
 > Cheers,
 > Sascha
 > 
 > 
 > Mathieu Giorgino wrote:
 > > Hello all,
 > > 
 > > I'm basically new to the ML part of Isabelle.
 > > 
 > > I'm defining a ML function to automatically generate specifications of an 
 > > Isabelle function (these specifications are given as argument to 
 > > Function_Fun.add_fun). During the generation, I obtain terms containing 
 > > schematic type variables. I need to constrain (with sorts) the types appearing 
 > > in these specifications, and I also transform the schematic type variables to 
 > > type variables (I think I have to).
 > > 
 > > However when I use this function in a locale, my generated type variables can 
 > > be the same as the locale's one (and a type capture occurs) which certainly 
 > > means I'm doing something wrong. What is the correct way to generate fresh 
 > > type variables (TFree) ?
 > > 
 > > I've searched through the Isabelle Cookbook and the sources 
 > > (Pure/{type.ML,term.ML,Isar/*local*}) without any real clue. Have I to collect 
 > > type variables of current locale fixed terms and use Name.variant ?
 > > 
 > > Thanks,
 > > 
 > > Mathieu





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.