[Agda] 'Dummie' question - why records?

[James Chapman]

Do we have intentional manifest fields in Agda?

Nisse explained at AIM how definitions in records are de-sugared using let. But, I've already forgotten.

Can somebody more knowledgable/less forgetful enlighten me how this works again?

We also discussed at AIM how it would be nice to beef up let to allow definitions by pattern matching. This would be useful in records as currently one can only define constants essentially (f x = y is just the constant f = \ x -> y).

Cheers,

James

On Oct 26, 2011, at 5:17 PM, Jean-Philippe Bernardy wrote:

> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda