comparison src/Equality.v @ 285:bd7f8720a691

Typo fix
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 07:56:30 -0500
parents 19fbda8a8117
children 540a09187193
comparison
equal deleted inserted replaced
284:693897f8e0cb 285:bd7f8720a691
732 ]] *) 732 ]] *)
733 733
734 rewrite (UIP_refl _ _ x0); reflexivity. 734 rewrite (UIP_refl _ _ x0); reflexivity.
735 Qed. 735 Qed.
736 736
737 (** 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. 737 (** 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.
738 738
739 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. *) 739 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. *)
740 (* end thide *) 740 (* end thide *)
741 741
742 742