[isabelle] Combining locales



Sorry if I posted this question already a few month ago:

Having a locale with two parameters

 locale A =
   fixes X :: "'a"
   fixes Y :: "'a"

I want to derive a locale from that, where the type of the parameters is constrained, for example:
 locale B = A +
   constrains X :: "'a list"

this will result in the error message:
*** exception TYPE raised: unify_parms: failed to unify types ?'a and 'b
*** At command "locale".

Whereas
 locale B = A +
   assumes "False ==> X = (X::('a list))"

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

gives the expected result. Is there any reason for the first declaration to fail ? 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.

Greeting and thanks in advance for any hints
 Peter Lammich








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