Email Gateway (Aug 08 2022 at 11:02): Email Gateway (Aug 08 2022 at 11:02):From: Robert Soeldner <cl-isabelle-users@lists.cam.ac.uk>
Hi,
based on Wenda Lis feedback on Zulip [1], I post the question here too.
In the following example, the first print_interps A` will list my
interpretation. The second one will print not.
Even when changing to sublocale A 1, the situation does not change.
To me, this behaviour is not expected. Any comment is welcome.
KR, Robert
locale A =
fixes x :: nat
locale B
begin
interpretation a: A 1 .
print_interps A
end
context B begin
print_interps A
end
Email Gateway (Aug 08 2022 at 16:34):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Robert,
The behaviour is actually expected. An interpretation of a locale is
only valid until the surrounding context ends. If you want to
permanently establish the interpretation, you should use the sublocale
command instead.
locale B begin
sublocale a: A 1 .
end
Hope this helps
Andreas
Am 08.08.2022 um 13:01 schrieb Robert Soeldner (via cl-isabelle-users
Mailing List):
Email Gateway (Aug 08 2022 at 18:39):From: Robert Soeldner <cl-isabelle-users@lists.cam.ac.uk>
Hi Andreas,
thank you for the explanation. The behaviour is the same for the
sublocale command. The first print_interp highlights the interpretation,
the second one reports on no interpretation. Is this due to the
print_interp command being more restrictive?
Email Gateway (Aug 12 2022 at 13:39):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Robert,
you're right. I can't really tell why print_interp behaves differently after leaving and
entering the locale context again. This may be some implementation detail that the locale
implementors may be able to answer.
From a practical point, all declarations in locale A are available in context B
independent of whether print_interp shows the interpretation as active.
Best,
Andreas
Last updated: Jan 04 2025 at 20:18 UTC