[Agda] `let' in record decl

[Andreas Abel]

On 11.10.12 7:44 PM, Serge D. Mechveliani wrote:
> 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?

I hope so...

Andreas

> 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
> [..]
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/