[Agda] binder for existential quantifier

[Jean-Philippe Bernardy]

See

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

in

http://www.cse.chalmers.se/~nad/listings/lib-0.5/Data.Product.html

Cheers,
-- JP


On Fri, Apr 8, 2011 at 11:08 AM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> Dear Agda list members,
>
> If I define the existential quantifier as follows:
>
>  Ω = Set -- type of propositions
>
>  data ∃ {X : Set} (A : X → Ω) : Ω where
>    ∃-intro : (x₀ : X) → A x₀ → ∃(\(x : X) → A x)
>
> then I have to write
>
>  ∃(\(x : X) → A x)       (*)
>
> rather than
>
>  ∃ (x : X) → A x         (**)
>
> as one can do with the universal quantifier.
>
> This is tolerable, but I would prefer to be able to write (**).
>
> Can this be done with a "syntax" declaration?
>
> Thanks,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>