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