# HG changeset patch # User Adam Chlipala # Date 1289393790 18000 # Node ID bd7f8720a691d327df0df7528fb8517e9f15be7e # Parent 693897f8e0cb21802213bf87544663f9afb44535 Typo fix diff -r 693897f8e0cb -r bd7f8720a691 src/Equality.v --- a/src/Equality.v Fri Nov 05 13:48:39 2010 -0400 +++ b/src/Equality.v Wed Nov 10 07:56:30 2010 -0500 @@ -734,7 +734,7 @@ rewrite (UIP_refl _ _ x0); reflexivity. Qed. -(** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always intercovert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. +(** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always interconvert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. *) (* end thide *)