Email Gateway (Jun 23 2022 at 13:55): Email Gateway (Jun 23 2022 at 13:55):From: Steven Obua <obua@practal.com>
I am wondering how to achieve the following: I have a locale
locale sigloc =
fixes S :: "signature"
and another locale
locale algloc =
fixes AA :: "'a algebra"
begin
definition S :: "signature" where
"S = Sig AA"
end
I would now like to declare algloc to be a sublocale of sigloc, such that
S = Sig AA
holds and S refers both to the algloc S and the sigloc S. I've tried something like
context algloc begin
sublocale sigloc "Sig AA"
end
but I don't think that works the way I would like it to work, as AA is treated just as a variable then. I don't want to do just
locale algloc = sigloc +
fixes AA :: "'a algebra"
because then algloc takes two parameters (S and AA) instead of just one (AA). Is there an easy/standard way to do this?
Cheers,
Steven
Email Gateway (Jun 23 2022 at 17:41):From: Steven Obua <obua@practal.com>
Thank you Richard,
that is exactly what I thought I was looking for! But it does not immediately help with my problem, unfortunately. Actually, I was mistaken in my earlier description of the problem, the sublocale instantiation works as I would want it to work, but the syntax of the super locale definition is not automatically transferred to the sub locale, which led to my confusion (see picture below). The syntax transfer does also not work with Richard's syntax.
Is there a way to transfer the syntax of definitions automatically?
Cheers,
Steven
image.png
Email Gateway (Jun 23 2022 at 19:01):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Steven,
No, you need to redeclare the syntax in this case.
Syntax is not transferred if the involved parameters are renamed or
instantiated. This is to avoid syntax conflicts when there are two
(distinct) instances of a locale active in the same context.
Clemens
Email Gateway (Jun 23 2022 at 19:39):From: Steven Obua <obua@practal.com>
Hi Clemens!
Ok, that certainly makes sense for the general case. Although, it would be nice to have the option to override that for special cases, for example if the syntax
locale B = A "k*3" for k :: nat
is used which Richard proposed, then I would expect syntax inheritance.
Cheers,
Steven
Last updated: Jan 04 2025 at 20:18 UTC