How to disable the -conversion in term parsing, which converts the term to . It's sometimes an obstacle to syntax translations.
As an illustration, I copied the exact code used for sets from the system theory src/HOL/Set.thy
(line 43 in Isabelle2021),
definition Collect :: "('a ⇒ bool) ⇒ 'a set" where "Collect = undefined"
translations
"{x. P}" ⇌ "CONST Collect (λx. P)"
It works for all situations except the case of where it's printed as rather than the expected , due to the unexpected aggressive -conversion.
However it's the exact code used in system theory, and is handled by the system theory rather well, printed as .
(Actually, I copied the whole theory Set.thy
from the system source, but the copied version still doesn't work.)
It's really confusing that what the magic is taken by the system theory? And how could I disable the embarrassing -conversion to let the version of mine work?
term "Collect (λx. P x)"
prints in the system version but in the copied version.
It must be some magic, translations "{x. P}" ⇌ "CONST Set.Collect (λx. P)"
works but translations "{x. P}" ⇌ "CONST My.Collect (λx. P)"
not. The magic should be applied to the Set.Collect
constant.
Last updated: Jul 15 2022 at 23:21 UTC