Re: [isabelle] Locale interpretation destroys sublocale
interpretation A ["sn" "ve" "vn"] by(unfold_locales,simp add:sn_def
If we now try again to look at B, the following happens:
*** Duplicate definition of (co)inductive predicate "local.P_Q_R.S"
*** The error(s) above occurred in locale: A P Q R
*** At command "print_locale".
What happens here is that after the interpretation a global inductive
definition is around. This happens to have the same name
(local.P_Q_R.S) as the inductive definition added to the local
context when evaluating locale A during print_locale B.
This is a bug, presumably due to inaccurate handling of names which
leads to fauly set up of the theory/context data of the inductive
For now you can get around this by adding a name prefix in the
interpretation my_label: A ["sn" "ve" "vn"]
This archive was generated by a fusion of
Pipermail (Mailman edition) and