Changeset 362 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 2, 2010, 11:53:49 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r357 r362 30 30 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). 31 31 32 notation "hvbox(l break !!! break n)" 33 non associative with precedence 90 34 for @{ 'get_index_v $l $n }. 35 32 36 (* ===================================== *) 33 37 (* Lookup. *) 34 38 (* ===================================== *) 35 39 36 nlet rec get_index (A: Type[0]) (n: Nat)40 nlet rec get_index_v (A: Type[0]) (n: Nat) 37 41 (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝ 38 42 (match m with … … 45 49 (match v return λx.λ_. S o < x → A with 46 50 [ Empty ⇒ λprf: S o < Z. ? 47  Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?51  Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ? 48 52 ]) 49 53 ]) lt. … … 54 58 nqed. 55 59 56 nlet rec get_index_weak (A: Type[0]) (n: Nat)60 nlet rec get_index_weak_v (A: Type[0]) (n: Nat) 57 61 (v: Vector A n) (m: Nat) on m ≝ 58 62 match m with … … 65 69 match v with 66 70 [ Empty ⇒ Nothing A 67  Cons p hd tl ⇒ get_index_weak A p tl o68 ] 69 ]. 70 71 interpretation "Vector get_index" 'get_index v n = (get_index? ? v n).71  Cons p hd tl ⇒ get_index_weak_v A p tl o 72 ] 73 ]. 74 75 interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n). 72 76 73 77 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
Note: See TracChangeset
for help on using the changeset viewer.