Email Gateway (Aug 22 2022 at 16:34): Email Gateway (Aug 22 2022 at 16:34):From: Diego Marmsoler <diego.marmsoler@tum.de>
Dear Isabelle Experts,
I have a question regarding concrete syntax for locales for which I need help.
Assuming that I create a new Isabelle locale by instantiating two other locales and adding some assumptions:
locale new_locale =
ml1: my_locale <parameters> + ml2: my_locale <parameters>
for <parameter notation> +
fixes <new notation for parameters>
assumes <something>
Assuming further that my_locale has some definitions which I want to use to specify the assumptions of new_locale.
Say, for example, it has a binary operator with infix syntax “_+_”.
Now, my question is whether I can change this infix syntax to be different for ml1 and ml2. For example, I want “_*_” as infix for ml1 and “_#_” for ml2.
I know that I can change it in within the locale (using notation). Then, however, I cannot use it for the definition of the assumptions of the locale.
Maybe someone can help.
Thanks and best regards,
Diego
smime.p7s
Email Gateway (Aug 22 2022 at 16:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Diego,
If the syntax is attached to the parameters of the locale (instead of proper definitions
inside the locales), you can specify new syntax in the for clause as in
for my_parameter (infix "+" 123)
This is not possible for definitions, though. If you really need this, you should split
your locale definition into two:
locale new_locale_aux =
ml1: my_locale <parameters> +
ml2: my_locale <parameters>
for <parameter notation>
begin
<declare new syntax for imported definitions>
end
locale new_locale = new_locale_aux +
fixes <more parameters>
assumes <something>
Unless you peek into the internal constructions and record-keeping of locales, the version
with two locales should behave the same as the version with one locale.
Hope this helps,
Andreas
Last updated: Apr 19 2024 at 04:17 UTC