Re: [isabelle] Combining Locales and specializing types

Clemens Ballarin wrote:

Peter wrote:

I have two locales:
 locale A =
   fixes f :: "'a => 'b"

 locale B =
   fixes g :: "'b => bool"

Now I want to combine these two, so that the types 'b in A and B are the same.

Type constraints on parameters may be added with the context element constrains:

 locale C = A + B +
   constrains f :: "'a => 'b"
     and g :: "'b => bool"

does what you want.

Thank you, that helped.
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".

But the typing of x should be clear from the declaration in A and the constraint on f (isn't it ?).


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