Re: [isabelle] type_synonym
On Thu, 9 Aug 2012, Tobias Nipkow wrote:
type_synonym 'a t = "'a :: field"
Ignoring sort constraints in type variables(s): "'a"
in type abbreviation "t"
Why that? It would be very nice not to lose them.
Can you explain what you are trying to achieve? Do you want the system to
reject type expressions if the argument types of synonyms do not observe
the sort constraint?
Type classes never restrict the domain of type constructors, they are
always defined. Type synonyms are not even type constructors, just some
abstract syntax for existing types.
This archive was generated by a fusion of
Pipermail (Mailman edition) and