Re: [isabelle] type_synonym



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.