Mercurial > cpdt > repo

comparison src/Predicates.v @ 488:31258618ef73

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Incorporate feedback from Nathan Collins
author Adam Chlipala <adam@chlipala.net>
date Tue, 08 Jan 2013 14:38:56 -0500
parents 1fd4109f7b31
children 07f2fb4d9b36
comparison
equal deleted inserted replaced
487:8bfb27cf0121 488:31258618ef73
127 (** %\vspace{-.15in}% [[ 127 (** %\vspace{-.15in}% [[
128 not = fun A : Prop => A -> False 128 not = fun A : Prop => A -> False
129 : Prop -> Prop 129 : Prop -> Prop
130 ]] 130 ]]
131 131
132 We see that [not] is just shorthand for implication of [False]. We can use that fact explicitly in proofs. The syntax [~ P] expands to [not P]. *) 132 We see that [not] is just shorthand for implication of [False]. We can use that fact explicitly in proofs. The syntax [~ P] %(written with a tilde in ASCII)% expands to [not P]. *)
133 133
134 Theorem arith_neq' : ~ (2 + 2 = 5). 134 Theorem arith_neq' : ~ (2 + 2 = 5).
135 (* begin thide *) 135 (* begin thide *)
136 unfold not. 136 unfold not.
137 (** [[ 137 (** [[