coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] First Order Logic - Propositional Function

From: Elvet <evil_grunger AT hotmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] First Order Logic - Propositional Function
Date: Wed, 15 Apr 2009 12:17:39 -0700 (PDT)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hey,

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!

Cheers,

Pete
--
View this message in context:
http://www.nabble.com/First-Order-Logic---Propositional-Function-tp23065352p23065352.html
Sent from the Coq mailing list archive at Nabble.com.

[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�