Re: [isabelle] instance declaration problem with axiomatic classes
Michael Norrish schrieb:
It seems that I cannot do the following
instance tyop :: (class1, class2) myclass
instance tyop :: (class3, class4) myclass
<some other proof>
where there is no connection between the various class<n>. This is
despite the fact that the proofs themselves do work.
My reading of the "Order-Sorted Unification" paper suggests to me that
I'm bumping my head against the "unnecessarily strong" co-regularity
condition. Is there any prospect of this being weakened?
Did I write "unnecessarily strong"? Because I don't think it is. If
(during type inference) you unify a type of class myclass with a type
"('a,'b) tyop", in your example it is not clear what the classes of the
subtypes 'a and 'b should be. You have lost the principal types property.
This archive was generated by a fusion of
Pipermail (Mailman edition) and