[isabelle] Conflict of type arities: What are the constraints on class instantiations?
I have naively tried to define a type-class for types that have more
than one element. However, when trying to make the obvious
instantiations, I get stuck with "Conflict of type arities" error
messages. I could not find any documentation on what the restrictions
are that I'm violating here, and how they are motivated. Any pointers?
instance prod :: (not_singleton,type) not_singleton ..
instance prod :: (type,not_singleton) not_singleton
Conflict of type arities:
prod :: (type, not_singleton) not_singleton and
prod :: (not_singleton, type) not_singleton
This archive was generated by a fusion of
Pipermail (Mailman edition) and