Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (9 years ago)
Author:
mulligan
Message:

less axioms

File:
1 edited

Legend:

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

    r340 r350  
    165165    ].
    166166
    167 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
    168                       (n: Nat) (f: A → B → C → C) (c: C)
    169                       (v: Vector A n) (q: Vector B n) on v
    170   (match v return λx.λ_. x = n → C with
     167nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])
     168                      (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)
     169                      (v: Vector A n) (q: Vector B n) on v : C n
     170  (match v return λx.λ_. x = n → C n with
    171171    [ Empty ⇒
    172       match q return λx.λ_. Z = x → C with
     172      match q return λx.λ_. Z = x → C x with
    173173        [ Empty ⇒ λprf: Z = Z. c
    174         | Cons o hd tl ⇒ λabsd. ?
     174        | Cons o hd tl ⇒ λabsd.
    175175        ]
    176176    | Cons o hd tl ⇒
    177       match q return λx.λ_. S o = x → C with
    178         [ Empty ⇒ λabsd: S o = Z. ?
     177      match q return λx.λ_. S o = x → C x with
     178        [ Empty ⇒ λabsd: S o = Z.
    179179        | Cons p hd' tl' ⇒ λprf: S o = S p.
    180             fold_right_i A B C o f (f hd hd' c) tl ?
     180           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉
    181181        ]
    182182    ]) (refl ? n).
    183     ##[##1,2:
    184         ndestruct;
    185     ##| ndestruct (prf);
    186         napply tl';
    187     ##]
     183 ndestruct; //.
    188184nqed.
    189185 
Note: See TracChangeset for help on using the changeset viewer.