[Agda] `let' in record decl

[Nils Anders Danielsson]

On 2012-10-10 17:44, Nicolas Pouillard wrote:
>    * 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

We already allow the following notation:

   id : let ★ = Set in (A : ★) → A → A
   id A x = x

I don't think we should introduce a second notation for the same thing.

>    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

Would it be hard to adopt the following notation instead?

   module MEndo let open Star in (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
>        ...

I think this short-cut should be dropped (because it is less natural
with the let ... in syntax).

-- 
/NAD