[Agda] `let' in record decl

Serge D. Mechveliani mechvel at botik.ru
Thu Oct 11 19:44:40 CEST 2012

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 



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 
>>    http://hub.darcs.net/np/Agda-TelescopingLet/patch/20121010151753-eb2e9

More information about the Agda mailing list