[Agda] `let' in record decl

[Andreas Abel]

On 11.10.2012 10:56, Nils Anders Danielsson wrote:
> 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.

I think the example is badly chosen.  let-in does not work in data type 
or module telescopes. E.g.

   data D (S : Setoid) (let A = Setoid.Carrier)(a : A) : A -> Set where

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

Frankly, I think your notation is more confusing...

>>    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).

But maybe the "let" should be dropped instead, e.g.,

   data D (A : Setoid)(A = Setoid.Carrier)(a : A) : A -> Set where

Since "=" is reserved, I do not see why this should not be parseable.

Summary:  Have three different telescope entries:

   x : A
   x = t
   open M args

This is somewhat like Matita (which have 1 and 2 as far as I know).

Cheers,
Andreas

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