Stream: Beginner Questions

Topic: disable eta-contraction in printing


view this post on Zulip 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 λx.Px\lambda x. P\,x is η\eta-contracted to PP.

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.

view this post on Zulip Qiyuan Xu (Jul 12 2021 at 04:31):

(deleted)

view this post on Zulip Qiyuan Xu (Jul 12 2021 at 05:15):

(deleted)

view this post on Zulip 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: Aug 13 2022 at 07:19 UTC