Ignore:
Timestamp:
Nov 26, 2010, 1:28:13 PM (9 years ago)
Author:
mulligan
Message:

get_arg_16 complete.

File:
1 edited

Legend:

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

    r272 r311  
    133133nqed.
    134134
    135 nlet rec split (A: Type[0]) (n,m: Nat) on m
     135nlet rec split (A: Type[0]) (m,n: Nat) on m
    136136             : Vector A (m+n) → (Vector A m) × (Vector A n)
    137137
     
    142142      [ Empty ⇒ λK.⊥
    143143      | Cons o he tl ⇒ λK.
    144          match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     144         match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
    145145          [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    146146//; ndestruct; //.
Note: See TracChangeset for help on using the changeset viewer.