Changeset 342 for Deliverables
- 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.