Changeset 340 for Deliverables
 Timestamp:
 Nov 30, 2010, 2:36:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r329 r340 28 28 for ${fold right @'vnil rec acc @{'vcons $x $acc}}. 29 29 30 notation "hvbox(hd break ::: tl)" 31 right associative with precedence 52 32 for @{ 'vcons $hd $tl }. 33 30 34 interpretation "Vector vnil" 'vnil = (Empty ?). 31 35 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). 32 interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).33 36 34 37 (* ===================================== *) … … 78 81 match v return λx.λ_. Z < x → Vector A x with 79 82 [ Empty ⇒ λabsd1: Z < Z. Empty A 80  Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl)83  Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl) 81 84 ] 82 85  S o ⇒ 83 86 (match v return λx.λ_. S o < x → Vector A x with 84 87 [ Empty ⇒ λprf: S o < Z. Empty A 85  Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?)88  Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?) 86 89 ]) 87 90 ]) lt. … … 135 138  Cons o he tl ⇒ λK. 136 139 match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with 137 [ mk_Cartesian v1 v2 ⇒ 〈he:: v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].140 [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 138 141 //; ndestruct; //. 139 142 nqed. … … 200 203 match v with 201 204 [ Empty ⇒ Empty B 202  Cons n hd tl ⇒ (f hd) :: (map A B n f tl)205  Cons n hd tl ⇒ (f hd) ::: (map A B n f tl) 203 206 ]. 204 207 … … 212 215  Cons m hd' tl' ⇒ 213 216 λe: S n = S m. 214 (f hd hd') :: (zip_with A B C n f tl ?)217 (f hd hd') ::: (zip_with A B C n f tl ?) 215 218 ] 216 219 ]) … … 240 243 match n return λn. Vector A n with 241 244 [ Z ⇒ Empty A 242  S m ⇒ h :: (replicate A m h)245  S m ⇒ h ::: (replicate A m h) 243 246 ]. 244 247 … … 247 250 match v return (λn.λv. Vector A (n + m)) with 248 251 [ Empty ⇒ q 249  Cons o hd tl ⇒ hd :: (append A o m tl q)252  Cons o hd tl ⇒ hd ::: (append A o m tl q) 250 253 ]. 251 254 … … 258 261 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat) 259 262 (f: A → B → A) (a: A) (v: Vector B n) on v ≝ 260 a :: 263 a ::: 261 264 (match v with 262 265 [ Empty ⇒ Empty A … … 310 313 match l return λl. Vector A (length A l) with 311 314 [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A) 312  Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))315  Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl)) 313 316 ]. 314 317 nnormalize.
Note: See TracChangeset
for help on using the changeset viewer.