[Agda] `let' in record decl

[Serge D. Mechveliani]

I understand all this as follows.

1. The Language Council includes the construct of  
                                     let-bounds in a telescope  
   (a certain reasonable variant of it) into the language standard.
2. It will be implemented (in MAlonzo ? in ... ?)
   in the official Agda release next to 2.3.0.1. 

Right?

Regards,
Sergei


On Thu, Oct 11, 2012 at 12:18:24AM +0200, Andreas Abel wrote:
> That sounds very nice!
>
> Can let-bound identifiers in a telescope get a type signature?
>
> On 10.10.12 5:44 PM, Nicolas Pouillard wrote:
>> On Wed 10 Oct 2012 - 19:08:44 [+0400], Serge D. Mechveliani wrote:
>>> On Wed, Oct 10, 2012 at 02:45:14PM +0200, Nils Anders Danielsson wrote:
>>>> On 2012-10-10 12:16, Serge D. Mechveliani wrote:
>>>>> Dear Agda developers,
>>>>> it is desirable to extend the language with a construct which enables to
>>>>> abbreviate such parts in a record/type declaration.
>>
>> This afternoon, with Daniel Gustafsson, we've done exactly this. This was
>> actually something annoying us as well. Especially to open modules.
[..]
>> We have implemented/tested/documented this feature as one branch sitting 
here:
>>    http://hub.darcs.net/np/Agda-TelescopingLet/patch/20121010151753-eb2e9
[..]