diff src/Predicates.v @ 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 f05514cc6c0d
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 *)