Mercurial > cpdt > repo
diff src/Equality.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 | b441010125d4 |
line wrap: on
line diff
--- a/src/Equality.v Thu Dec 09 14:30:24 2010 -0500 +++ b/src/Equality.v Thu Dec 09 14:39:49 2010 -0500 @@ -80,7 +80,7 @@ ]] - The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *) + The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term substituted. *) cbv zeta. (** [[ @@ -297,7 +297,7 @@ ]] - The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering to the [in]-bound variable [x']. To do a dependent [match], we %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq]. We are just as constrained to use the %``%#"#real#"#%''% value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity. + The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x']. To do a dependent [match], we %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq]. We are just as constrained to use the %``%#"#real#"#%''% value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity. Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)