Ignore:
Timestamp:
Nov 26, 2010, 6:13:26 PM (9 years ago)
Author:
mulligan
Message:

Added fold_right_i, equivalent of O'Caml's fold_right2.

File:
1 edited

Legend:

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

    r316 r320  
    159159    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
    160160    ].
     161   
     162nlet 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    ]) ?.
    161179   
    162180nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.