Email Gateway (Aug 22 2022 at 16:26): Email Gateway (Aug 22 2022 at 16:26):From: Peter Lammich <lammich@in.tum.de>
Hi list,
Is there a way to produce localized mixfix rules?
For example, I have the following
syntax
"_mylist" :: "args => 'a list" ("⦇(_)⦈")
translations
"⦇x, xs⦈" ⇌ "x#[xs]"
"⦇x⦈" ⇌ "x#[]"
However, I would like to "activate" this syntax only inside a locale
(or bundle), in order not to pollute the global syntax space too much.
However, writing
bundle MySyntax begin
syntax
"_mylist" :: "args => 'a list" ("⦇(_)⦈")
yields an "invalid context for syntax command" error. The same when I try inside a locale.
Also the attempt
syntax
"_mylist" :: "args => 'a list"
bundle MySyntax begin
notation "_mylist" ("⦇(_)⦈")
fails with an "unknown constant" error.
Thanks in advance for any help,
Peter
Last updated: Apr 26 2024 at 16:20 UTC