Re: [Agda] : vs. ∶

Andrew Pitts Andrew.Pitts at
Fri May 4 17:53:19 CEST 2012

On 4 May 2012 16:37, Martin Escardo <m.escardo at> 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...


More information about the Agda mailing list