Changeset 368 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 2, 2010, 6:27:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r364 r368 422 422 λv: Vector A n. 423 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. 424 fold_right ? ? ? (λx, v. conjunction v (fold_right ? ? ? (λy, z. inclusive_disjunction z (f x y)) false q)) true v. 428 425 429 426 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.