Changeset 248 for Deliverables/D4.1/Matita/List.ma
 Timestamp:
 Nov 22, 2010, 11:43:04 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r247 r248 5 5 include "Util.ma". 6 6 include "Universes.ma". 7 include "Bool.ma". 7 8 include "Nat.ma". 8 9 (* include "Maybe.ma". *) … … 39 40 (* Lookup. *) 40 41 (* ===================================== *) 41 42 43 (* 42 44 nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝ 43 45 match n with … … 84 86 ] 85 87 ]. 88 *) 86 89 87 90 (* ===================================== *) … … 205 208 ]. 206 209 207 nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l ≝208 match l with 209 [ Empty ⇒ False210 nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝ 211 match l with 212 [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0) 210 213  Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl) 211 214 ]. … … 318 321 nelim l. 319 322 nnormalize. 320 napplyS append_empty_left_neutral. 323 nrewrite > (append_empty_left_neutral ? ?). 324 @. 321 325 #H L A. 322 326 nnormalize. 323 327 nrewrite > A. 324 napplyS append_associative. 328 nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))). 329 @. 325 330 nqed. 326 331 … … 378 383 #H L H2. 379 384 nnormalize. 380 //. 385 nrewrite > H2. 386 @. 381 387 nqed. 382 388 … … 391 397 #H L H2. 392 398 nnormalize. 393 //. 394 nqed. 395 399 nrewrite > H2. 400 @. 401 nqed. 402 403 (* 396 404 nlemma empty_get_index_nothing: 397 405 ∀A: Type[0]. … … 404 412 //. 405 413 nqed. 414 *) 406 415 407 416 nlemma rotate_right_empty:
Note: See TracChangeset
for help on using the changeset viewer.