Changeset 315
 Timestamp:
 Nov 26, 2010, 5:32:34 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r314 r315 185 185 nqed. 186 186 187 ndefinition eq_bv ≝ 188 λn: Nat. 189 λb, c: BitVector n. 190 eq_v Bool n (λd, e. 191 if inclusive_disjunction (conjunction d e) (conjunction (negation d) 192 (negation e)) then 193 true 194 else 195 false) b c. 196 187 197 naxiom plus_minus_inverse_left: 188 198 ∀m, n: Nat. 
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.