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

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

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

> As far as I can tell, the result is a > unification of two previously distinct constants, split and prod_case. I > must confess that this duplication has never bothered me. Just to make it clear, this distinction is extinct since approx. 2009. What remains is a quite mechanical and

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

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

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

Dear Florian, I get the definite impression that the whole operation is out of proportion wrt the benefits. As far as I can tell, the result is a unification of two previously distinct constants, split and prod_case. I must confess that this duplication has never bothered me. Now the

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

Like, next week I do want to try to unify of_nat and real. Larry > On 22 Sep 2015, at 15:39, Tobias Nipkow wrote: > > I would prefer to leave things as they are now. That print translation is ok > and you would be moving the complications elsewhere. We really have more >