[Agda] `let' in record decl

[Nicolas Pouillard]

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,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20121010/4722d806/attachment-0002.bin