[Agda] no-eta-equality

[Wolfram Kahl]

On Wed, Sep 28, 2016 at 03:16:56PM +0200, Nils Anders Danielsson wrote:
> On 2016-09-28 15:07, Andrea Vezzosi wrote:
> >However you should also consider the following version, so that
> >(suc'Rd (rd a n)) does not reduce by itself, but only when projections
> >are applied to it.
> >
> > [...]
> 
> I think sucRd is more readable than suc'Rd, and I don't think we should
> encourage people to obfuscate their code in order to make it faster. A
> better alternative might be to devise some way to instruct Adga to do
> this kind of rewrite behind the scenes.

Strongly agreed!


Wolfram