Re: [Agda] : vs. ∶

[Jean-Philippe Bernardy]

On Fri, May 4, 2012 at 5:09 PM, Wolfgang Jeltsch
<g9ks157k at acme.softbase.org> wrote:
> Hello,
>
> I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
> to be similar to :. However, I think this similarity is precisely its
> weakness. You cannot tell from looking at the code whether your code is
> syntactically correct or not. Furthermore, there is a semantic problem.
> The symbol ∶ is called RATIO, but Σ does not have anything to do with
> ratios. I propose to use an alternative syntax, maybe the following:
>
>    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
>
> What do others think?

My original intention with 'syntax' was to allow:

syntax Σ A (∀ x → B) = (x : A) × B

(Note the forall, "real" parens and "real" colon).

This could maybe be re-considered.

Cheers,
JP.