[Agda] no-eta-equality

[Nils Anders Danielsson]

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.
>
> suc'Rd :  {A : Set} → Rd A → Rd A
> fl1 (suc'Rd (rd a n)) =  a
> fl2 (suc'Rd (rd a n)) = n

The last occurrence of n should be replaced by suc n.

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.

-- 
/NAD