[Agda] : vs. ∶

[Wolfgang Jeltsch]

Am Donnerstag, den 29.11.2012, 08:41 -0600 schrieb Alan Jeffrey:
> 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. In particular, the Σ[ x : A ] B would use the regular COLON 
> rather than RATIO.
> 
> Alan.

Yes, generalizing the “syntax” construct in such a way is probably a
much better solution.

Best wishes,
Wolfgang