Re: [isabelle] How to obtain all type variables declared in a proof context?



Am 14.07.2019 um 18:03 schrieb mailing-list anonymous:
> I am trying to obtain a list of all type variables that are declared
> in a proof context. It does not seem that the relevant data is exposed to
> the public interface.

Yes, I think this is not exposed. As I understand it, it is more of an
implementation detail, and the "invent fresh names" operations are what
you are supposed to use.

[...]

> The use case is the generation of fresh schematic type variables.

In this case, I would probably generate fixed type variables first (cf.
Variable.invent_types) and then generalize the final results (terms,
theorems) (cf. Variable.export_*)

Hope this helps

Alex




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