[isabelle] private behaves strangely in locales
The qualifier private behaves strangely inside locales. If I have a private constant
definition (say foo) in a locale (say l1) and want to define a constant of the same name
in a sublocale (say l2), I get an error about local.foo being declared twice if and only
if both definitions depend on parameters of the locale. As the private modifier should
ensure that the first declaration does not leave the scope of the unnamed context block, I
would have expected Isabelle to accept this always.
Below is a minimal example. If you change any of the defining equations to "foo = ()",
Isabelle2015 accepts them. As is, I get the error. Is there anything else I can do other
than choosing different names?
locale l1 = fixes n :: unit begin
private definition foo where "foo = n"
locale l2 = l1 + assumes "True" begin
definition foo where "foo = n" (* error duplicate constant declaration *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and