[Agda] Pattern matching weirdness?

[Pierre Hyvernat]

>If you want eta-expansion of ∑, you should define it as a "record", as 
>in the standard library.
>
OK.
However, using record prevents you from defining functions by pattern 
matching, doesn't it?


>So: feature.
>
Mmm...
Is there a reason we don't want eta-expansion on data (surjective 
pairing), or is this just an implementation artefact?


Pierre
-- 
Reality is that which, when you stop believing in it,
doesn't go away.
    -- Philip K. Dick