[Agda] Pattern matching weirdness?

[Jean-Philippe Bernardy]

If you want eta-expansion of ∑, you should define it as a "record", as
in the standard library.
So: feature.

Cheers,
JP.