coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Syntax question ...

From: Satrajit Roy <satrajit.roy AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Syntax question ...
Date: Wed, 9 Feb 2011 17:51:40 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=lC6BYmpQz9KcTbjiakh0mEw2hiYw9Pq5S/dZDFx1ZnQTB3ZYKjOHvodeOAad9DO96u Thlt371Pvn2MQ16uu1bPRNDzqnWKllVITkjPfFc+pIPS9g3N3oXDqtQ9oWBBk3NPGaxz MZ95Q90ytc45CD0X1sMJfNUmlhH7Hd1sT2TCg=

What is the correct way to express statements like the following in the Coq environment?

for all x, exists y such that A(x, y) =>� exists y, for all x such that A(x, y) and the converse of it
--

Satrajit

[Coq-Club] Syntax question ..., Satrajit Roy
- Re: [Coq-Club] Syntax question ..., Evgeny Makarov
- [Coq-Club] Re: Syntax question ..., Satrajit Roy
  - Re: [Coq-Club] Re: Syntax question ..., Pierre Casteran
  - Re: [Coq-Club] Re: Syntax question ..., roconnor