Re: [isabelle] Combining locales



On 1 Aug 2006, at 13:57, Peter Lammich wrote:

Is there any reason for the first declaration to fail ?

The reason is, of course, rooted in the implementation. Unlike assumes, constrains elements currently don't fully participate in type inference. This phenomenon should disappear eventually.

The second one is obviously a "dirty hack", while the 3rd one can be tedious to write down if having many fixed parameters with related types.

 locale B = A +
   constrains X :: "'a list"
   constrains Y :: "'a list"

You shouldn't worry about this too much. There are not many examples of useful locales where parameter types are instances of another locale, and that do not have any additional assumptions. (Endomorphisms vs. Homomorphisms is one.)

Clemens






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