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



Dear All,

Today, I found myself struggling to resolve a, seemingly, very trivial
issue. 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. However, most likely, I am missing something.

Here is a minimal example:

val ctxt = @{context};
val T = TVar (("'a", 0), ["Groups.plus"]);
val ctxt = Variable.declare_typ T ctxt;
(* val declTs = obtain_declared_types ctxt ? *)

Please note that I am aware of the function Variable.is_declared. However,
seemingly, this function merely performs a check based on the name context
and, therefore, does not include the schematic (type) variables.

The use case is the generation of fresh schematic type variables.
Therefore, if a solution to this problem can already be found somewhere in
the source code, it may be a suitable alternative to the answer to the
original question. Nevertheless, I would still highly prefer to understand
how to obtain all declared type variables.

Thank you

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



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