Changeset 350 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 1, 2010, 1:10:53 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r340 r350 165 165 ]. 166 166 167 nlet rec fold_right _i (A: Type[0]) (B: Type[0]) (C:Type[0])168 ( n: Nat) (f: A → B → C → C) (c: C)169 (v: Vector A n) (q: Vector B n) on v ≝170 (match v return λx.λ_. x = n → C with167 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0]) 168 (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat) 169 (v: Vector A n) (q: Vector B n) on v : C n ≝ 170 (match v return λx.λ_. x = n → C n with 171 171 [ Empty ⇒ 172 match q return λx.λ_. Z = x → C with172 match q return λx.λ_. Z = x → C x with 173 173 [ Empty ⇒ λprf: Z = Z. c 174  Cons o hd tl ⇒ λabsd. ?174  Cons o hd tl ⇒ λabsd. ⊥ 175 175 ] 176 176  Cons o hd tl ⇒ 177 match q return λx.λ_. S o = x → C with178 [ Empty ⇒ λabsd: S o = Z. ?177 match q return λx.λ_. S o = x → C x with 178 [ Empty ⇒ λabsd: S o = Z. ⊥ 179 179  Cons p hd' tl' ⇒ λprf: S o = S p. 180 fold_right_i A B C o f (f hd hd' c) tl ?180 (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉ 181 181 ] 182 182 ]) (refl ? n). 183 ##[##1,2: 184 ndestruct; 185 ## ndestruct (prf); 186 napply tl'; 187 ##] 183 ndestruct; //. 188 184 nqed. 189 185
Note: See TracChangeset
for help on using the changeset viewer.