Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML
- To: mailing-list anonymous <mailing.list.anonymous at gmail.com>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML
- From: Alexander Krauss <krauss at in.tum.de>
- Date: Wed, 1 May 2019 13:16:05 +0200
- In-reply-to: <CALaF1UL9FJe8dftUWQg6Z6dPtdW4FNo73mqS2AbhQ=+H1jz4cw@mail.gmail.com>
- References: <CALaF1UL9FJe8dftUWQg6Z6dPtdW4FNo73mqS2AbhQ=+H1jz4cw@mail.gmail.com>
- User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1
(re-sending as I forgot to Cc the list)
Am 01.05.2019 um 01:06 schrieb mailing-list anonymous:
> I would like to understand if there exists a canonical method for creating
> cterms with automatic type inference from several distinct terms in
> Isabelle/ML, given that some of these distinct terms are supplied by the
I there is not really a well-established canonical method, since the
needs of tools are quite different in the details.
What tools usually do is try to get to a "fully typed" stage as soon as
possible in the outermost layers, and then work with full type
information internally, which means that you must usually carry types
What I would try is this:
* Make sure you get the user-provided constants / terms in a polymorphic
version, i.e., with schematic type variables. Here, the function
"Variable.polymorphic" should help.
* Then, construct the combined terms as you need them, and run type
checking on this. (-> Syntax.check_terms). I think this should
instantiate the type variables properly.
* Then you should get terms on which Thm.cterm_of should work.
Note that Syntax.check_terms includes several specific things like
insertion of coercions etc. But it is the most general answer to "how do
I check / infer types".
Hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and