Changeset 320


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.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r315 r320  
    228228    ].
    229229   
    230 naxiom half_add:
    231   ∀n: Nat.
    232   ∀b, c: BitVector n.
    233     Bool × (BitVector n).
    234    
    235230naxiom full_add:
    236231  ∀n: Nat.
     
    238233  ∀d: Bit.
    239234    Bool × (BitVector n).
     235   
     236ndefinition half_add ≝
     237  λn: Nat.
     238  λb, c: BitVector n.
     239    full_add n b c false.
  • 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.