Changeset 349 for Deliverables/D4.1/Matita/List.ma
 Timestamp:
 Dec 1, 2010, 11:18:05 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r342 r349 216 216 ]. 217 217 218 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 219 (f: A → B → C → C) (c: C) 220 (l: List A) (r: List B) (p: length ? l = length ? r) on l: C ≝ 221 (match l return λx. (length ? x) = (length ? r) → C with 222 [ Empty ⇒ 223 match r return λx. Z = length ? x → C with 224 [ Empty ⇒ λprf: Z = Z. c 225  Cons hd tl ⇒ λabsd. ? 226 ] 227  Cons hd tl ⇒ 228 match r return λx. S (length ? tl) = length ? x → C with 229 [ Empty ⇒ λabsd: S(length ? tl) = Z. ? 230  Cons hd' tl' ⇒ λprf: S(length ? tl) = length ? (hd'::tl'). 231 fold_right_i A B C f (f hd hd' c) tl tl' ? 232 ] 233 ]) p. 234 ##[##1,2: 235 nnormalize in absd; 236 ndestruct (absd); 237 ####3: 238 nnormalize in prf; 239 ndestruct (prf); 240 nassumption; 241 ##] 242 nqed. 243 218 244 nlet rec fold_left (A: Type[0]) (B: Type[0]) 219 245 (f: A → B → A) (x: A) (l: List B) on l ≝ … … 223 249 ]. 224 250 225 nlet rec fold_left i_aux (A: Type[0]) (B: Type[0])251 nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0]) 226 252 (f: Nat → A → B → A) (x: A) (i: Nat) (l: List B) on l ≝ 227 253 match l with 228 254 [ Empty ⇒ x 229  Cons hd tl ⇒ f i (fold_left i_aux A B f x (S i) tl) hd230 ]. 231 232 ndefinition fold_left i ≝ λA,B,f,x. fold_lefti_aux A B f x Z.255  Cons hd tl ⇒ f i (fold_left_i_aux A B f x (S i) tl) hd 256 ]. 257 258 ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x Z. 233 259 234 260 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.