[Agda] Re: 'Dummie' question - why records?

Jean-Philippe Bernardy bernardy at chalmers.se
Wed Oct 26 16:17:51 CEST 2011


On Wed, Oct 26, 2011 at 3:49 PM, Zhaohui Luo <zhaohui.luo at hotmail.co.uk> wrote:
> People in this thread may be interested in the following paper of mine on
> dependent record types

I would welcome integration of some of this in Agda.
In particular I think that well-designed DRTs should be able to subsume modules,
and I think you make a good case for that.

Cheers,
JP.


More information about the Agda mailing list