[Agda] 'Dummie' question - why records?

Dirk Ullrich dirk.ullrich at googlemail.com
Mon Oct 17 19:27:17 CEST 2011

Hallo Agdanistas,

maybe this is a stupid question: Why do we have, beside type
declarations using `data', declarations for record types by `record'
in Agda?
1. Cannot, at least in principle, any n-fold record type be replaced
by an appropriate n-fold product over the same types?
2. If the anwser to 1. is yes: what is the rationale of having
`record' beside `data'?


More information about the Agda mailing list