[Agda] `let' in record decl

[Nils Anders Danielsson]

On 2012-10-11 11:51, Andreas Abel wrote:
> On 11.10.2012 10:56, Nils Anders Danielsson wrote:

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

Well, typically you don't start with a let:

   module M {A B : Set}
            (f : A → B)
            let open X f in
            (p : P f)
            where

> But maybe the "let" should be dropped instead, e.g.,
>
>    data D (A : Setoid)(A = Setoid.Carrier)(a : A) : A -> Set where

I assume that you don't want to drop let from the syntax of expressions.
I don't want to use different notation for the same thing, depending on
whether I happen to be writing a telescope or an expression.

> Summary:  Have three different telescope entries:
>
>    x : A
>    x = t
>    open M args

I think I would find this more appealing if "let" was removed entirely
(but that would be a rather disruptive change).

-- 
/NAD