Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interpretation in locale context


view this post on Zulip 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

[1]
https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Interpretation.20in.20locale.20context

view this post on Zulip 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):

view this post on Zulip 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?

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC