[Agda] 'Dummie' question - why records?

Nils Anders Danielsson nad at chalmers.se
Tue Oct 18 11:05:55 CEST 2011

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


More information about the Agda mailing list