Changeset 315 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 26, 2010, 5:32:34 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r311 r315 362 362 λa: A. 363 363 iterate (Vector A n) (λx. shift_right_1 A n x a) v m. 364 365 (* ===================================== *) 366 (* Decidable equality. *) 367 (* ===================================== *) 368 369 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b ≝ 370 (match b return λx.λ_. n = x → Bool with 371 [ Empty ⇒ 372 match c return λx.λ_. x = Z → Bool with 373 [ Empty ⇒ λ_. true 374  Cons p hd tl ⇒ λabsd.? 375 ] 376  Cons o hd tl ⇒ 377 match c return λx.λ_. x = S o → Bool with 378 [ Empty ⇒ λabsd. ? 379  Cons p hd' tl' ⇒ 380 λprf. 381 if (f hd hd') then 382 (eq_v A o f tl ?) 383 else 384 false 385 ] 386 ]) (refl ? n). 387 ##[##1, 3: 388 ndestruct (absd); 389 ndestruct (prf); 390 napply tl'; 391 ####2: 392 ndestruct (absd); 393 ##] 394 nqed. 364 395 365 396 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.