Mercurial > cpdt > repo
comparison src/Equality.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 14:23:52 -0400 |
| parents | 4320c1a967c2 |
| children | 40a9a36844d6 |
comparison
equal
deleted
inserted
replaced
| 474:d9e1fb184672 | 475:1fd4109f7b31 |
|---|---|
| 178 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality "as data." *) | 178 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality "as data." *) |
| 179 | 179 |
| 180 | 180 |
| 181 (** * Heterogeneous Lists Revisited *) | 181 (** * Heterogeneous Lists Revisited *) |
| 182 | 182 |
| 183 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *) | 183 (** One of our example dependent data structures from the last chapter was the heterogeneous list and its associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *) |
| 184 | 184 |
| 185 Section fhlist. | 185 Section fhlist. |
| 186 Variable A : Type. | 186 Variable A : Type. |
| 187 Variable B : A -> Type. | 187 Variable B : A -> Type. |
| 188 | 188 |