HuanSun (Dec 07 2022 at 14:18): HuanSun (Dec 07 2022 at 14:18):I want to develop a more elegant symbolic system for my work. I want to provide syntax for Apure bexp, so I tried as Apure bexp ("⟨_⟩" [40] 40) . It works fine. However, If I want to do some composition, for instance, conjunction or disjunction, I need to write something like (⟨b1⟩) /\ (⟨b2⟩) which looks unclear. So can I define a syntax for (Apure bexp) with brackets so that I don't need annoying brackets in my expression.
Jan van Brügge (Dec 09 2022 at 14:56):If you increase the numbers in your syntax definition it will bind tighter. You could try 60 instead of 40
Wolfgang Jeltsch (Dec 09 2022 at 18:54):I think you could actually leave out any binding information altogether. This way, Isabelle will accept terms with any binding strength within the brackets (the binding strength of the argument terms has to be at least the smallest possible binding strength, which is 0) and will consider the term with the brackets to have the largest possible binding strength, which is 1000. That’s generally the best approach towards bracketing structures, I think, as the brackets leave no room for ambiguities.
Last updated: Apr 24 2024 at 08:20 UTC