coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] First Order Logic - Propositional Function

From: Adam Chlipala <adamc AT hcoop.net>
To: Elvet <evil_grunger AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] First Order Logic - Propositional Function
Date: Mon, 20 Apr 2009 10:08:14 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Elvet wrote:

How can I represent a propositional function in Coq? Something along the
lines of:

Ex Q(x)
(where E is supposed to be the existential quantifier)

I'm sure this is trivial, but I am totally lost!

Which source (book, etc.) are you using to learn Coq? Any good introduction will cover this. (I'm guessing, because your question confuses me, and I'm not sure exactly what you're asking.)

[Coq-Club] First Order Logic - Propositional Function, Elvet
- Re: [Coq-Club] First Order Logic - Propositional Function, Adam Chlipala
  - Re: [Coq-Club] First Order Logic - Propositional Function, Yves Bertot
- Re: [Coq-Club] First Order Logic - Propositional Function, Marko Malikovi�