Mercurial > cpdt > repo
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 447:9e3333bd08a1 | 448:2740b8a23cce |
|---|---|
| 847 | 847 |
| 848 | 848 |
| 849 (* begin hide *) | 849 (* begin hide *) |
| 850 (* In-class exercises *) | 850 (* In-class exercises *) |
| 851 | 851 |
| 852 (* 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. *) | 852 (* 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. *) |
| 853 | 853 |
| 854 (* begin thide *) | 854 (* begin thide *) |
| 855 Inductive prop : Set := | 855 Inductive prop : Set := |
| 856 | Tru : prop | 856 | Tru : prop |
| 857 | Fals : prop | 857 | Fals : prop |