Changeset 342
 Timestamp:
 Nov 30, 2010, 4:46:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r331 r342 222 222  Cons hd tl ⇒ f (fold_left A B f x tl) hd 223 223 ]. 224 225 nlet rec fold_lefti_aux (A: Type[0]) (B: Type[0]) 226 (f: Nat → A → B → A) (x: A) (i: Nat) (l: List B) on l ≝ 227 match l with 228 [ Empty ⇒ x 229  Cons hd tl ⇒ f i (fold_lefti_aux A B f x (S i) tl) hd 230 ]. 231 232 ndefinition fold_lefti ≝ λA,B,f,x. fold_lefti_aux A B f x Z. 224 233 225 234 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.