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
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