Re: [isabelle] type_synonym

On Fri, 10 Aug 2012, Tobias Nipkow wrote:

I meant on the Isabelle top level. Like command "typ". But with class.

Here are some variants with terms, using the regular type-inference to ensure a certain sort membership in the end:

term "TYPE('a::finite * 'b::finite * bool) :: _::finite itself"

  let "_ :: _::finite itself" = "TYPE('a::finite * 'b::finite * bool)"

This works because "_::finite" is a type-inference parameter that can be instantiated.

In principle, one could cook up something like SORT_CONSTRAINT for the above, although that is not that elegant.

This is just type-inference, not sort-inference. And without the term context, there would not even be type-inference.


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