Mercurial > cpdt > repo
changeset 203:71ade09024ac
Quibbly note on [eq] in first-order logic
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 04 Jan 2009 08:18:59 -0500 |
| parents | 8caa3b3f8fc0 |
| children | cbf2f74a5130 |
| files | src/Predicates.v |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Predicates.v Sat Jan 03 19:57:02 2009 -0500 +++ b/src/Predicates.v Sun Jan 04 08:18:59 2009 -0500 @@ -354,7 +354,7 @@ ex_intro : forall x : A, P x -> ex P ]] *) -(** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. *) +(** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic. For our purposes, it is. *) Theorem exist1 : exists x : nat, x + 1 = 2. (* begin thide *)