Changeset 229


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

More changes.

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

Legend:

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

    r228 r229  
    11include "Maybe.ma".
    22include "Nat.ma".
     3include "Util.ma".
    34
    45ninductive List (A: Type[0]): Type[0] ≝
     
    2021  match l with
    2122    [ Empty ⇒ Z
    22     | Cons hd tl ⇒ S (length A tl)
     23    | Cons hd tl ⇒ S $ length A tl
    2324    ].
    2425   
     
    6566  match l with
    6667    [ Empty ⇒ Empty A
    67     | Cons hd tl ⇒ reverse A tl @ (Cons A hd (Empty A))
     68    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    6869    ].
    6970   
     
    8788  match n with
    8889    [ Z ⇒ Empty A
    89     | S o ⇒ a :: (replicate A o a)
     90    | S o ⇒ a :: replicate A o a
    9091    ].
  • 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.