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
This archive was generated by a fusion of
Pipermail (Mailman edition) and