# Changeset 340 for Deliverables

Ignore:
Timestamp:
Nov 30, 2010, 2:36:20 PM (9 years ago)
Message:

::: is now used in place of :: for vectors to reduce ambiguity

File:
1 edited

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

 r329 for \${fold right @'vnil rec acc @{'vcons \$x \$acc}}. notation "hvbox(hd break ::: tl)" right associative with precedence 52 for @{ 'vcons \$hd \$tl }. interpretation "Vector vnil" 'vnil = (Empty ?). interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) match v return λx.λ_. Z < x → Vector A x with [ Empty ⇒ λabsd1: Z < Z. Empty A | Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl) | Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl) ] | S o ⇒ (match v return λx.λ_. S o < x → Vector A x with [ Empty ⇒ λprf: S o < Z. Empty A | Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?) | Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?) ]) ]) lt. | Cons o he tl ⇒ λK. match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. //; ndestruct; //. nqed. match v with [ Empty ⇒ Empty B | Cons n hd tl ⇒ (f hd) :: (map A B n f tl) | Cons n hd tl ⇒ (f hd) ::: (map A B n f tl) ]. | Cons m hd' tl' ⇒ λe: S n = S m. (f hd hd') :: (zip_with A B C n f tl ?) (f hd hd') ::: (zip_with A B C n f tl ?) ] ]) match n return λn. Vector A n with [ Z ⇒ Empty A | S m ⇒ h :: (replicate A m h) | S m ⇒ h ::: (replicate A m h) ]. match v return (λn.λv. Vector A (n + m)) with [ Empty ⇒ q | Cons o hd tl ⇒ hd :: (append A o m tl q) | Cons o hd tl ⇒ hd ::: (append A o m tl q) ]. nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat) (f: A → B → A) (a: A) (v: Vector B n) on v ≝ a :: a ::: (match v with [ Empty ⇒ Empty A match l return λl. Vector A (length A l) with [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A) | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl)) | Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl)) ]. nnormalize.
Note: See TracChangeset for help on using the changeset viewer.