Stream: Beginner Questions

Topic: disable eta-contraction in printing

Qiyuan Xu (Jul 12 2021 at 04:25):

How to disable the $\eta$-contraction when print terms?
For example,

translations "{x. P}" ⇌ "CONST MyCollect (λx. P)"

this translation works in every case except the {x. P x}.
For {x. P x}, it is printed as MyCollect P because the $\lambda x. P\,x$ is $\eta$-contracted to $P$.

In the reference manual, it is mentioned that such $\eta$-contracted can be prevented by print-translations in ML, but there is no further information about this.

Qiyuan Xu (Jul 12 2021 at 04:31):

(deleted)

Qiyuan Xu (Jul 12 2021 at 05:15):

(deleted)

Qiyuan Xu (Jan 24 2022 at 06:05):

Finally, i found the solution when i read the source Set.thy. The eta contraction is disabled by print_translations

print_translation ‹
 [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹Ball› \<^syntax_const>‹_Ball›,
  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹Bex› \<^syntax_const>‹_Bex›]
› ― ‹to avoid eta-contraction of body›

Last updated: Apr 16 2024 at 12:28 UTC