Ignore:
Timestamp:
Dec 2, 2010, 4:36:35 PM (9 years ago)
Author:
mulligan
Message:

Added subvector_with function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vector.ma

    r363 r364  
    410410        napply tl' ]
    411411nqed.
     412
     413(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     414(* Subvectors.                                                                *)
     415(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     416
     417ndefinition subvector_with ≝
     418  λA: Type[0].
     419  λn: Nat.
     420  λm: Nat.
     421  λf: A → A → Bool.
     422  λv: Vector A n.
     423  λq: Vector A m.
     424    let list_q ≝ list_of_vector A m q in
     425    let list_v ≝ list_of_vector A n v in
     426    let power ≝ power_list A list_q in
     427      member_with ? list_v (λx, y. eq_l ? f x y) power.
    412428   
    413429(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.