Mercurial > cpdt > repo
changeset 271:aa3c054afce0
Some bug fixes while working on JFR version
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 19 Apr 2010 16:49:26 -0400 |
parents | fd46d077b952 |
children | 19fbda8a8117 |
files | src/Equality.v src/Subset.v |
diffstat | 2 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Equality.v Wed Feb 03 08:17:02 2010 -0500 +++ b/src/Equality.v Mon Apr 19 16:49:26 2010 -0400 @@ -574,7 +574,7 @@ (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial. - Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *) + Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *) Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x), O = match pf with refl_equal => O end.
--- a/src/Subset.v Wed Feb 03 08:17:02 2010 -0500 +++ b/src/Subset.v Mon Apr 19 16:49:26 2010 -0400 @@ -71,7 +71,7 @@ (** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0. When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match. When [n] is a successor, we have no need for the proof and just return the answer. The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n]. -One aspects in particular of the definition of [pred_strong1] that may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. +One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. [[ Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=