Re: [isabelle] Generating fresh type variables

On Wed, 29 Jun 2011, Mathieu Giorgino wrote:

Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't realized it can also be used for types. If I understand correctly, type variables and term variables are in the same namespace (implicitly separated by the prefix "'") ?

No you should not do that. Term variables and type variables are different things. You probably mean Variable.invent_types, or even the import operations that will put things into context without manual fiddling.

By the way, thanks for the Isabelle Cookbook, it's really helpful to start with Isabelle/ML.

It is certainly helpful, but you always need to cross-check with other sources of information. Many fine points in the cookbook are not exactly right.


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