[Agda] binder for existential quantifier

[Martin Escardo]

Wonderful. Many thanks, JP.
Martin

On 08/04/11 12:02, Jean-Philippe Bernardy wrote:
> 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
>>