[Agda] `let' in record decl
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Oct 11 11:51:47 CEST 2012
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/
More information about the Agda
mailing list