[Agda] `let' in record decl

Nicolas Pouillard np at nicolaspouillard.fr
Thu Oct 11 21:41:46 CEST 2012

On Thu 11 Oct 2012 - 21:44:40 [+0400], Serge D. Mechveliani wrote:
> I understand all this as follows.
> 2. It will be implemented (in MAlonzo ? in ... ?)

So far this has no connection with what's happening in MAlonzo.
On one hand this is because these lets are substituted away before
MAlonzo sees them and on the other hand this means that this will
work with MAlonzo out of the box.

Nicolas Pouillard

More information about the Agda mailing list