Stream: Beginner Questions

Topic: Interpretation in locale context


view this post on Zulip Robert Soeldner (Aug 08 2022 at 09:26):

I do have the follow example:

locale A =
  fixes x :: nat

locale B
begin

interpretation a: A 1 .

print_interps A
end

context B begin
  print_interps A
end

The first print_interps A will list my interpretation a. The second (in the context of B) says: no interpretations
I would assume, this is not expected?

view this post on Zulip Wenda Li (Aug 08 2022 at 10:27):

To me, with the interpretation keyword the interpretation is temporary (i.e., the interpretation will be lost after exiting the begin-end block), so that the current behaviour is expected. However, even if we replace interpretation with sublocale that introduces a permanent link between B and A the final print_interps A still has no interpretations, which is not expected to me.

view this post on Zulip Wenda Li (Aug 08 2022 at 10:27):

It probably worth raising this question in the mailing list.

view this post on Zulip Robert Soeldner (Aug 08 2022 at 10:56):

Thank you Wenda


Last updated: Mar 28 2024 at 20:16 UTC