[Agda] 'Dummie' question - why records?

[Nils Anders Danielsson]

On 2011-10-26 16:48, James Chapman wrote:
> Do we have intentional manifest fields in Agda?

Randy Pollack showed how you can implement records with manifest fields
as a library (using induction-recursion). See the module Record in the
standard library for one implementation:

   http://www.cse.chalmers.se/~nad/listings/lib/README.Record.html
   http://www.cse.chalmers.se/~nad/listings/lib/Record.html

I don't know what "intentional" means in this context.

-- 
/NAD