Re: [isabelle] instance declaration problem with axiomatic classes



Michael Norrish schrieb:
It seems that I cannot do the following

   instance tyop :: (class1, class2) myclass
   <some proof>

   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.

Best
Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.