[Agda] no-eta-equality

[Andrea Vezzosi]

If we replace Rd with a type like Group or Category the version with
copatterns would actually be more readable, being closer to module
syntax.

People can decide where the trade-off between readability and
efficiency lands in their case.

The rewrite in question changes semantics, but I guess it could be
requested by the user with a pragma or some dedicated syntax.




On Wed, Sep 28, 2016 at 3:16 PM, Nils Anders Danielsson <nad at cse.gu.se> 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.
>>
>> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda