*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] type_synonym*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 10 Aug 2012 17:16:09 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1208101653300.3776@macbroy21.informatik.tu-muenchen.de>*References*: <50240E48.5090403@in.tum.de> <alpine.LNX.2.00.1208092251590.19061@macbroy21.informatik.tu-muenchen.de> <50249F75.1030807@in.tum.de> <alpine.LNX.2.00.1208101632500.3776@macbroy21.informatik.tu-muenchen.de> <50251FD3.2010105@in.tum.de> <alpine.LNX.2.00.1208101653300.3776@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

I meant on the Isabelle top level. Like command "typ". But with class. Tobias Am 10/08/2012 17:04, schrieb Makarius: > On Fri, 10 Aug 2012, Tobias Nipkow wrote: > >>> What exactly means "to check"? What is the application context? >> >> Check in the sense of ascertain, test, verify. Writing T down and having it >> parsed settles only that it (T) is a legal type, but not if it is, for >> example, a field. > > Of course, one can do this in ML. So far I was under the implicit assumption > that we talk about type inference for the surface syntax that is usually exposed > to end-users. > > > Here is an example: > > ML {* > val T = @{typ "'a::finite * 'b::finite * bool"}; > val S = @{sort finite}; > @{assert} (Sign.of_sort @{theory} (T, S)) > *} > > So T is first produced by going through the whole syntax + check layers of > Isabelle. Later we test if it belongs to a certain sort. > > Once could wrap something like this into a document antiquotation for example. > Note that it can *not* be done inside an ML syntax translation -- that is too > early in the many syntax layers and the information is not there yet. > > > Makarius

**Follow-Ups**:**Re: [isabelle] type_synonym***From:*Makarius

**References**:**[isabelle] type_synonym***From:*Tobias Nipkow

**Re: [isabelle] type_synonym***From:*Makarius

**Re: [isabelle] type_synonym***From:*Tobias Nipkow

**Re: [isabelle] type_synonym***From:*Makarius

**Re: [isabelle] type_synonym***From:*Tobias Nipkow

**Re: [isabelle] type_synonym***From:*Makarius

- Previous by Date: Re: [isabelle] type_synonym
- Next by Date: Re: [isabelle] isabelle/jedit
- Previous by Thread: Re: [isabelle] type_synonym
- Next by Thread: Re: [isabelle] type_synonym
- Cl-isabelle-users August 2012 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