Changeset 328 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 29, 2010, 11:17:58 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r322 r328 170 170 ]. 171 171 172 (*173 172 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 174 (n: Nat) (m: Nat) 175 (f: A → B → C → C) (c: C) 176 (v: Vector A n) (q: Vector B m) on v ≝ 177 (match v return λx.λ_. x = m → C with 173 (n: Nat) (f: A → B → C → C) (c: C) 174 (v: Vector A n) (q: Vector B n) on v ≝ 175 (match v return λx.λ_. x = n → C with 178 176 [ Empty ⇒ 179 177 match q return λx.λ_. Z = x → C with 180 [ Empty ⇒ λ _.c178 [ Empty ⇒ λprf: Z = Z. c 181 179  Cons o hd tl ⇒ λabsd. ? 182 180 ] 183 181  Cons o hd tl ⇒ 184 182 match q return λx.λ_. S o = x → C with 185 [ Empty ⇒ λabsd . ?183 [ Empty ⇒ λabsd: S o = Z. ? 186 184  Cons p hd' tl' ⇒ λprf: S o = S p. 187 fold_right_i A B C o p f (f hd hd') tl tl' 188 ] 189 ]) ?. 190 *) 185 fold_right_i A B C o f (f hd hd' c) tl ? 186 ] 187 ]) (refl ? n). 188 ##[##1,2: 189 ndestruct; 190 ## ndestruct (prf); 191 napply tl'; 192 ##] 193 nqed. 191 194 192 195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) … … 207 210  Cons n hd tl ⇒ (f hd) :: (map A B n f tl) 208 211 ]. 209 210 (* Should be moved into Plogic/equality.ma at some point. Only Type[2] version211 currently in there.212 *)213 nlemma eq_rect_Type0_r :214 ∀A: Type[0].215 ∀a:A.216 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.217 #A a P H x p.218 ngeneralize in match H.219 ngeneralize in match P.220 ncases p.221 //.222 nqed.223 212 224 213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) … … 477 466 @. 478 467 nqed. 479 480 naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.
Note: See TracChangeset
for help on using the changeset viewer.