[Agda] `let' in record decl

[Nicolas Pouillard]

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
http://nicolaspouillard.fr