Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bundled or Localized "syntax"

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC