[Agda] 'Dummie' question - why records?

[Dirk Ullrich]

Hallo Jesper,

2011/10/18 Jesper Louis Andersen <jesper.louis.andersen at gmail.com>:
> On Tue, Oct 18, 2011 at 11:05, Nils Anders Danielsson <nad at chalmers.se> wrote:
>
>> One might wonder why we don't simply implement η-equality for, say,
>> non-recursive single-constructor data types. One reason is that, while
>> there are many situations in which η-equality is nice to have, there are
>> some where it's nice not to have η. Ulf's "inspect on steroids" is one
>> example.
>
> I've never heard about η-equality. η-expansion for the lambda calculus
> yes, but not equality. Are the two related in any way?
Eta-equality is the equivalence relation generated by eta-expansion.

Dirk