Changeset 363 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 2, 2010, 2:03:48 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r362 r363 58 58 nqed. 59 59 60 ndefinition get_index' ≝ 61 λA: Type[0]. 62 λn, m: Nat. 63 λb: Vector A (S (n + m)). 64 get_index_v A (S (n + m)) b n ?. 65 nnormalize; 66 napply less_than_or_equal_monotone; 67 napply less_than_or_equal_plus; 68 nqed. 69 60 70 nlet rec get_index_weak_v (A: Type[0]) (n: Nat) 61 (v: Vector A n) (m: Nat) on m ≝71 (v: Vector A n) (m: Nat) on m ≝ 62 72 match m with 63 73 [ Z ⇒
Note: See TracChangeset
for help on using the changeset viewer.