Ignore:
Timestamp:
Nov 9, 2010, 5:00:50 PM (9 years ago)
Author:
mulligan
Message:

More changes.

File:
1 edited

Legend:

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

    r228 r229  
    55include "Cartesian.ma".
    66include "Nat.ma".
     7include "Util.ma".
    78(* include "List.ma". *)
    89
     
    4445  match v with
    4546    [ Empty ⇒ Z
    46     | Cons n hd tl ⇒ S (length A n tl)
     47    | Cons n hd tl ⇒ S $ length A n tl
    4748    ].
    4849
     
    6970nqed.
    7071
    71 
    7272nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
    7373             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
     
    7777      match q return (λy.λr. S n = y → Vector C (S n)) with
    7878        [ Empty ⇒ ?
    79         | Cons m hd2 tl2
     79        | Cons m hd' tl'
    8080            λe: S n = S m.
    81               Cons C n (f hd hd2) (zip A B C n f tl ?)
     81              (f hd hd') :: (zip A B C n f tl ?)
    8282        ]
    8383    ])
     
    8585      ##
    8686        [ #e;
    87           ndestruct (e);
     87          ndestruct(e);
    8888          ##
    89         | ndestruct (e);
    90           napply tl2
     89        | ndestruct(e);
     90          napply tl'
    9191          ##
    9292        ]
Note: See TracChangeset for help on using the changeset viewer.