Re: [Agda] : vs. ∶

[Andrew Pitts]

On 4 May 2012 16:37, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> The ideal solution, however, would be so add Σ, Π, and ∃ as primitive, as
> was done with ∀, so that one can write Σ(x : X) → Y x, or Σ x → Y x.

I think Jean-Philippe's solution is more ideal than yours---I'd like
to be able to just write (x : A) × B for a dependent product type.

Concrete syntax, don't you just love it...

Andy