Stream: General

Topic: bundled syntax / translations

view this post on Zulip Kevin Kappelmann (Jul 13 2020 at 15:54):

Is there some way to bundle syntax and/or translations? Or is there some other way to provide a mechanism to enable and disable notations defined using syntax and translation in a structured approach?

For notations, I can do something like

bundle hotg_mem_syntax begin notation mem (infixl "∈" 50) end
bundle no_hotg_mem_syntax begin no_notation mem (infixl "∈" 50) end

unbundle hotg_mem_syntax

But what if I want to do something like

syntax
  "_ball"  :: ‹[idts, set, bool] ⇒ bool› ("(2∀_ ∈ _./ _)" 10)
  "_ball2" :: ‹[idts, set, bool] ⇒ bool›
translations
  "∀x xs ∈ A. P" ⇀ "CONST ball A (λx. _ball2 xs A P)"
  "_ball2 x A P" ⇀ "∀x ∈ A. P"
  "∀x ∈ A. P" ⇌ "CONST ball A (λx. P)"

?

Last updated: Apr 24 2024 at 12:33 UTC