Changeset 1646 for src/ASM/Vector.ma
 Timestamp:
 Jan 16, 2012, 3:04:14 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r1599 r1646 522 522 fold_right … (λy,v. (eq_a x y) ∨ v) false l. 523 523 524 525 definition subvector_with ≝ 526 λA: Type[0]. 527 λn: nat. 528 λm: nat. 529 λf: A → A → bool. 530 λv: Vector A n. 531 λq: Vector A m. 532 fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v. 524 let rec subvector_with 525 (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m) 526 on sub: bool ≝ 527 match sub with 528 [ VEmpty ⇒ true 529  VCons n' hd tl ⇒ 530 if mem … eq … sup hd then 531 subvector_with … eq tl sup 532 else 533 false 534 ]. 533 535 534 536 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.