*Subject*: Re: [isabelle] Canonical types of constants*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 9 Feb 2016 16:39:39 +0100*Cc*: Isabelle Users List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1602091312520.44291@lxbroy10.informatik.tu-muenchen.de>*References*: <56B99C57.3060706@in.tum.de> <alpine.LNX.2.00.1602091312520.44291@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

Thanks, that works fine. Tobias On 09/02/2016 13:22, Makarius wrote:

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

**Attachment:
smime.p7s**

**References**:**[isabelle] Canonical types of constants***From:*Tobias Nipkow

**Re: [isabelle] Canonical types of constants***From:*Makarius

- Previous by Date: Re: [isabelle] Canonical types of constants
- Next by Date: Re: [isabelle] Disk usage in ~/.isabelle/contrib
- Previous by Thread: Re: [isabelle] Canonical types of constants
- Next by Thread: [isabelle] [Isabelle2016-RC4] sledgehammer blocks metis proofs
- Cl-isabelle-users February 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list