Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]

[Nils Anders Danielsson]

On 2012-10-11 16:50, Andreas Abel wrote:
> On 11.10.2012 12:31, Nils Anders Danielsson wrote:
>> 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.
>
> I do not think it is very different notation.  The three telecope
> entries listed below are things you can use in a where block or at the
> top level.  There, you do not prefix bindings "x = t" with a let.

At the moment a syntactically valid telescope Γ is also a syntactically
valid expression "prefix": Γ → Set is syntactically valid, for instance.
I don't understand why you would want to break this property.

-- 
/NAD