Re: [isabelle] Generating fresh type variables



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.