Mercurial > cpdt > repo

comparison src/DataStruct.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 5f25705a10ea
children 97c60ffdb998
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
159 ]] 159 ]]
160 *) 160 *)
161 (* end thide *) 161 (* end thide *)
162 162
163 (* begin hide *) 163 (* begin hide *)
164 (* begin thide *)
164 Definition map' := map. 165 Definition map' := map.
166 (* end thide *)
165 (* end hide *) 167 (* end hide *)
166 168
167 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *) 169 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
168 170
169 Section ilist_map. 171 Section ilist_map.
235 end 237 end
236 | MCons _ _ x mls' => fun mem => 238 | MCons _ _ x mls' => fun mem =>
237 match mem in member ls' return (match ls' with 239 match mem in member ls' return (match ls' with
238 | nil => Empty_set 240 | nil => Empty_set
239 | x' :: ls'' => 241 | x' :: ls'' =>
240 B x' -> (member ls'' -> B elm) -> B elm 242 B x' -> (member ls'' -> B elm)
243 -> B elm
241 end) with 244 end) with
242 | MFirst _ => fun x _ => x 245 | MFirst _ => fun x _ => x
243 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem' 246 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
244 end x (hget mls') 247 end x (hget mls')
245 end. 248 end.
470 end. 473 end.
471 474
472 (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality. *) 475 (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality. *)
473 476
474 (* begin hide *) 477 (* begin hide *)
475 Definition foo := (@eq, @eq_refl). 478 (* begin thide *)
479 Definition foo := @eq_refl.
480 (* end thide *)
476 (* end hide *) 481 (* end hide *)
477 482
478 Print eq. 483 Print eq.
479 (** %\vspace{-.15in}% [[ 484 (** %\vspace{-.15in}% [[
480 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x 485 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x