Mercurial > cpdt > repo

comparison src/Subset.v @ 474:d9e1fb184672

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 13:48:45 -0400
parents 51a8472aca68
children 1fd4109f7b31
comparison
equal deleted inserted replaced
473:39c204d2262c 474:d9e1fb184672
170 match s with 170 match s with
171 | exist O pf => match zgtz pf with end 171 | exist O pf => match zgtz pf with end
172 | exist (S n') _ => n' 172 | exist (S n') _ => n'
173 end. 173 end.
174 174
175 (** To build a value of a subset type, we use the [exist] constructor, and the details of how to do that follow from the output of our earlier [Print sig] command (where we elided the extra information that parameter [A] is implicit). *) 175 (** To build a value of a subset type, we use the [exist] constructor, and the details of how to do that follow from the output of our earlier [Print sig] command, where we elided the extra information that parameter [A] is implicit. We need an extra [_] here and not in the definition of [pred_strong2] because _parameters_ of inductive types (like the predicate [P] for [sig]) are not mentioned in pattern matching, but _are_ mentioned in construction of terms (if they are not marked as implicit arguments). *)
176 176
177 Eval compute in pred_strong2 (exist _ 2 two_gt0). 177 Eval compute in pred_strong2 (exist _ 2 two_gt0).
178 (** %\vspace{-.15in}% [[ 178 (** %\vspace{-.15in}% [[
179 = 1 179 = 1
180 : nat 180 : nat
220 (* begin thide *) 220 (* begin thide *)
221 Definition pred_strong := 0. 221 Definition pred_strong := 0.
222 (* end thide *) 222 (* end thide *)
223 (* end hide *) 223 (* end hide *)
224 224
225 (** The function %\index{Gallina terms!proj1\_sig}%[proj1_sig] extracts the base value from a subset type. It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier. 225 (** A value in a subset type can be thought of as a%\index{dependent pair}% _dependent pair_ (or%\index{sigma type}% _sigma type_) of a base value and a proof about it. The function %\index{Gallina terms!proj1\_sig}%[proj1_sig] extracts the first component of the pair. It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier.
226 226
227 By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *) 227 By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *)
228 228
229 Extraction pred_strong3. 229 Extraction pred_strong3.
230 230