[Agda] `let' in record decl

[Serge D. Mechveliani]

On Wed, Oct 10, 2012 at 10:56:11AM +0200, Andreas Abel wrote:
[..]
> On 09.10.12 3:29 PM, Serge D. Mechveliani wrote:
>> Please, how to abbreviate  `Carrier ord'  in the declaration  of
>> ------------------------------------
>> record Merge1
>>    {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2)
>>    (m : Carrier ord) (xs : List $ Carrier ord) (ys : List $ Carrier ord)
>>                                          : Set (suc $ max c $ max l1 l2)
>>    where
>>    A = Carrier ord
>>    field list    : List A
>>          ordered : OrderedList? ord (m :: list)
>> ------------------------------------
>> ?
>> (Agda-2.3.0.1, MAlonzo).
>> [..]

> That is unfortunately not possible.  In a telescope (the bindings  
> between "Merge1" and ": Set...") one cannot use let in Agda (although it  
> would not be unthinkable).

Dear Agda developers,
it is desirable to extend the language with a construct which enables to 
abbreviate such parts in a record/type declaration.
Probably, it is needed to allow `let' or `where' in these telescopes.
The benefit costs the needed implementation effort.
And this will preserve correct the existing Agda programs.

The textual (macro) replacements 
(like   A ==> Carrier ord   written in a separate line)  
are easier to implement, but this is not so expressive.

Regards,
Sergei