[Agda] `let' in record decl

[Serge D. Mechveliani]

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.
>
> Please add a ticket for it on the bug tracker.


It has come out  issue 710.
It is on the bug tracker, but it is not actually about a bug,
it is a Suggestion for the Language.

Regards,
Sergei