[Agda] : vs. ∶

[Nils Anders Danielsson]

On 2012-11-29 15:41, Alan Jeffrey wrote:
> If we're chipping in opinions, then I'd like syntax declarations to be
> extended to allow patterns rather than just variables, for example
> something like:
>
>    syntax Σ _ (λ { P → B }) = Σ[ P ] B
>
> so that you can then write:
>
>    Σ[ x ] B
>    Σ[ x : A ] B
>    Σ[ x , y ] B
>
> etc. etc.

I don't follow you: "x : A" is not a pattern.

-- 
/NAD