Re: [isabelle] Combining Locales and specializing types

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.


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