[Agda] 'Dummie' question - why records?

[Nils Anders Danielsson]

On 2011-10-17 20:07, Daniel Peebles wrote:
> Records have eta, meaning in a sense that Agda "knows" that there's a
> constructor whenever it has a value of the record type.

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.

-- 
/NAD