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
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and