[Agda] 'Dummie' question - why records?
dirk.ullrich at googlemail.com
Mon Oct 17 19:27:17 CEST 2011
maybe this is a stupid question: Why do we have, beside type
declarations using `data', declarations for record types by `record'
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