[isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]
makarius at sketis.net
Wed Oct 7 16:33:29 CEST 2015
On Tue, 22 Sep 2015, Florian Haftmann wrote:
> 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.
The uncheck phase -- despite being introduced already in 2006/2007 -- is
not fully used as much as it could or should. Apart from eta contraction,
there are other fine points that I don't dare to dig up at the moment.
More information about the isabelle-dev