[isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]

[Florian Haftmann]

The situation turned out more complicated than anticipated: implicit
eta-contraction happens at a rather late level in the printing machinery
using a print translation. Hence, any countermeasure must act on the
same (or a later level). However in the ecosystem as it is today, it
seems better to do such transformations at the uncheck level, i.e. quite
close to the logic.

For the moment, I installed the print translation from e6b1236f9b3d
again to retain the previous behavior in af7bed1360f3. Please report
remaining suspicious behavior.

To get ahead from there, I need to understand more about eta-contracted
printing.

According to my current understanding, this has been introduced once to
produce less surprises if proof tools perform spontaneous eta-expansion
(please correct me if this is wrong).

To get more fine-grained control there, I can foresee two approaches:
a) Move the eta-contract machinery to the uncheck level also.
b) Provide a special syntactic marker which is »syntactic identity« but
does not perform eta-contraction on its immediate argument. This would
allow uncheckers to protect certain abstractions using this marker.

b) seems preferable, since there is less risk to produce unexpected
deviations from current printing without being noticed.

Comments?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150922/b3a85d75/attachment.sig>