Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (9 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

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

    r266 r268  
    55
    66include "Util.ma".
    7 
    8 include "Universes.ma".
    97
    108include "Nat.ma".
     
    133131    ].
    134132    //.
     133nqed.
     134
     135nlet rec split (A: Type[0]) (n,m: Nat) on m
     136             : Vector A (m+n) → (Vector A m) × (Vector A n)
     137
     138 match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with
     139  [ Z ⇒ λv.〈[[ ]], v〉
     140  | S m' ⇒ λv.
     141     match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
     142      [ Empty ⇒ λK.⊥
     143      | Cons o he tl ⇒ λK.
     144         match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     145          [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
     146//; ndestruct; //.
    135147nqed.
    136148   
Note: See TracChangeset for help on using the changeset viewer.