Changeset 342 for Deliverables


Ignore:
Timestamp:
Nov 30, 2010, 4:46:45 PM (9 years ago)
Author:
sacerdot
Message:

fold_lefti

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r331 r342  
    222222    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
    223223    ].
     224
     225nlet 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
     232ndefinition fold_lefti ≝ λA,B,f,x. fold_lefti_aux A B f x Z.
    224233   
    225234(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.