Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] private behaves strangely in locales

Email Gateway (Aug 22 2022 at 09:57):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 25 2024 at 20:15 UTC