[isabelle] private behaves strangely in locales



Dear Makarius,

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
context begin
private definition foo where "foo = n"
end
end

locale l2 = l1 + assumes "True" begin
definition foo where "foo = n" (* error duplicate constant declaration *)
end

Thanks,
Andreas




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