Re: [isabelle] Combining Locales and specializing types

Peter wrote:

Perhaps one should add, that one should constrain all parameters. I now have something like:
 locale A =
     f :: "'a set => 'l => 'l" and
     x :: "'l"

 locale B = A +
     f :: "'a set => 'l => 'l" and
     x :: "'l"
   fixes g :: "'a set list => 'l => 'l"

This works, but if I drop the type constraint on x, I get the error:
*** exception TYPE raised: unify_parms: failed to unify types ?'b and 'b
*** At command "locale".

Thanks for pointing this out.  This is probably a bug.


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