Mercurial > cpdt > repo
changeset 199:cadeb49dc1ef
Fix typo
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 01 Dec 2008 08:32:20 -0500 |
| parents | a35eaec19781 |
| children | df289eb8ef76 |
| files | src/Equality.v |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Equality.v Fri Nov 28 14:21:38 2008 -0500 +++ b/src/Equality.v Mon Dec 01 08:32:20 2008 -0500 @@ -25,7 +25,7 @@ (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's %\textit{%#<i>#definitional equality#</i>#%}%. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal. - The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [1] when applied to [0]. *) + The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *) Definition pred' (x : nat) := match x with