Re: [isabelle] Canonical types of constants

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 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 =
      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.


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