Mercurial > cpdt > repo
diff src/Predicates.v @ 448:2740b8a23cce
Proofreading pass through Chapter 3
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 17 Aug 2012 14:19:59 -0400 |
| parents | 89c67796754e |
| children | 79190c225f1a |
line wrap: on
line diff
--- a/src/Predicates.v Fri Aug 17 12:22:26 2012 -0400 +++ b/src/Predicates.v Fri Aug 17 14:19:59 2012 -0400 @@ -849,7 +849,7 @@ (* begin hide *) (* In-class exercises *) -(* EX: Define a type [prop] of simple boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction. Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula. Prove that every false-free [prop] is valid. *) +(* EX: Define a type [prop] of simple Boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction. Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula. Prove that every false-free [prop] is valid. *) (* begin thide *) Inductive prop : Set :=