[Agda] : vs. ∶

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

On 11/29/2012 04:10 AM, Nils Anders Danielsson wrote:
> On 2012-11-29 03:22, Andreas Abel wrote:
>> I'd prefer the RATIO symbol (fake colon) to the epsilon.
>
> Any other opinions?
>