Re: [isabelle] Locale interpretation destroys sublocale



Hi Daniel,

interpretation A ["sn" "ve" "vn"] by(unfold_locales,simp add:sn_def ve_def vn_def)

If we now try again to look at B, the following happens:

print_locale B

*** 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 package.

For now you can get around this by adding a name prefix in the interpretation command:

interpretation my_label: A ["sn" "ve" "vn"]

Clemens







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