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

  "_ball"  :: [idts, set, bool]  bool ("(2∀_ ∈ _./ _)" 10)
  "_ball2" :: [idts, set, bool]  bool
  "∀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: Aug 15 2022 at 02:13 UTC