Changeset 320 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 26, 2010, 6:13:26 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r316 r320 159 159  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 160 160 ]. 161 162 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 163 (n: Nat) (m: Nat) 164 (f: A → B → C → C) (c: C) 165 (v: Vector A n) (q: Vector B m) on v ≝ 166 (match v return λx.λ_. x = m → C with 167 [ Empty ⇒ 168 match q return λx.λ_. Z = x → C with 169 [ Empty ⇒ λ_.c 170  Cons o hd tl ⇒ λabsd. ? 171 ] 172  Cons o hd tl ⇒ 173 match q return λx.λ_. S o = x → C with 174 [ Empty ⇒ λabsd. ? 175  Cons p hd' tl' ⇒ λprf: S o = S p. 176 fold_right_i A B C o p f (f hd hd') tl tl' 177 ] 178 ]) ?. 161 179 162 180 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.