[Agda] `let' in record decl

[Andreas Abel]

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.
>
> I feared this could result in a very ugly patch but it was actually pretty
> simple to integrate.
>
> We have implemented/tested/documented this feature as one branch sitting here:
>    http://hub.darcs.net/np/Agda-TelescopingLet/patch/20121010151753-eb2e9
>
> To get it:
>    $ darcs get http://hub.darcs.net/np/Agda-TelescopingLet
>
> Documentation:
>
>    * Telescoping lets: Local bindings are now accepted in telescopes
>
>      The syntax of telescopes as been extended to support 'let':
>
>        id : (let ★ = Set) (A : ★) → A → A
>        id A x = x
>
>    In particular one can now 'open' modules inside telescopes:
>
>      module Star where
>        ★ : Set₁
>        ★ = Set
>
>      module MEndo (let open Star) (A : ★) where
>        Endo : ★
>        Endo = A → A
>
>    Finally a shortcut is provided for opening modules:
>
>      module N (open Star) (A : ★) (open MEndo A) (f : Endo) where
>        ...
>
> Best regards,
>

-- 
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/