Email Gateway (Aug 22 2022 at 12:52): Email Gateway (Aug 22 2022 at 12:52):From: Tobias Nipkow <nipkow@in.tum.de>
In order to obtain the type of a constant c I am using this code snippet:
Proof_Context.read_const {proper = true, strict = false} ctxt c
It gives me back a term Const(c,T) and then I proceed with T. How can I make
sure that the type variables in T have canonical names 'a, 'b etc? Should I be
using some other piece of code?
The background is that in 7f5579b12b0a, constant "card" has type "?'b set =>
nat" instead of "?'a set => nat" as in the past. I assume that I should not rely
on canonicity of names in T? If not, how can I convert a type into a `canonical'
one?
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 12:52):From: Makarius <makarius@sketis.net>
On Tue, 9 Feb 2016, Tobias Nipkow wrote:
In order to obtain the type of a constant c I am using this code snippet:
Proof_Context.read_const {proper = true, strict = false} ctxt c
It gives me back a term Const(c,T) and then I proceed with T. How can I make
sure that the type variables in T have canonical names 'a, 'b etc? Should I
be using some other piece of code?
This correctly produces a type scheme for the constant, according to its
declaration. It uses schematic type variables, but these are considered
"private" to a declaration and not necessarily canonical in an application
context.
The proper way to make schematics visible in a context (and printable) can
be seen in the implementation of the document antiquotation @{const}:
Variable.import_terms.
Note that show_question_marks = false produces unreliable results:
pretending that schematic variables are not schematic is fragile.
LaTeXsugar.thy seems to suffer from that wrong assumption.
The background is that in 7f5579b12b0a, constant "card" has type "?'b
set => nat" instead of "?'a set => nat" as in the past.
The definition of "card" has changed here
http://isabelle.in.tum.de/repos/isabelle/rev/9f4f0dc7be2c and thus its
internal type declaration.
Here is an example that illustrates the situation and shows how to make
canonical types inside a given context:
consts a :: 'a
consts b :: 'b
ML ‹
fun read_const ctxt s =
let
val t = Proof_Context.read_const {proper = true, strict = false} ctxt s;
val ([t'], _) = Variable.import_terms true [t] ctxt;
in (t, t') end;
read_const @{context} "a";
read_const @{context} "b";
read_const @{context} "card";
›
Of course, the result depends on the context. E.g. within the context of
"context fixes x :: 'a begin" new types start at 'b.
Makarius
Email Gateway (Aug 22 2022 at 12:52):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, that works fine.
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC