Re: [isabelle] type_synonym



There would probably not be that many uses of such a document antiquotation but
surely one could also wrap that code up into a top level command?

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





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