Mercurial > cpdt > repo
comparison src/DataStruct.v @ 296:559ec7328410
Spelling errors found preparing JFR paper
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 09 Dec 2010 14:39:49 -0500 |
| parents | 1b6c81e51799 |
| children | 7b38729be069 |
comparison
equal
deleted
inserted
replaced
| 295:6833a1b778c0 | 296:559ec7328410 |
|---|---|
| 781 (fun idx => cfold (bodies idx)) | 781 (fun idx => cfold (bodies idx)) |
| 782 (* end thide *) | 782 (* end thide *) |
| 783 end. | 783 end. |
| 784 | 784 |
| 785 (* begin thide *) | 785 (* begin thide *) |
| 786 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly-automated one, with the only wrinkle being a guided instantation of the quantifiers in the induction hypothesis. *) | 786 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly-automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *) |
| 787 | 787 |
| 788 Lemma cfoldCond_correct : forall t (default : exp' t) | 788 Lemma cfoldCond_correct : forall t (default : exp' t) |
| 789 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t), | 789 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t), |
| 790 exp'Denote (cfoldCond default tests bodies) | 790 exp'Denote (cfoldCond default tests bodies) |
| 791 = exp'Denote (Cond n tests bodies default). | 791 = exp'Denote (Cond n tests bodies default). |