Stream: Beginner Questions

Topic: Interpretation in locale context

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?

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.

Wenda Li (Aug 08 2022 at 10:27):

It probably worth raising this question in the mailing list.

Robert Soeldner (Aug 08 2022 at 10:56):

Thank you Wenda

Last updated: Dec 21 2024 at 16:20 UTC