Changeset 2124 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (8 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r2122 r2124  
    223223 vsplit' A m n v.
    224224
    225 lemma vsplit_ok:
    226   ∀A: Type[0].
    227   ∀m, n: nat.
    228   ∀v: Vector A (m + n).
    229   ∀upper: Vector A m.
    230   ∀lower: Vector A n.
    231     〈upper, lower〉 = vsplit A m n v →
    232       upper @@ lower = v.
    233   #A #m #n #v #upper #lower
    234   cases daemon
    235 qed.
    236 
    237225lemma vsplit_zero:
    238226  ∀A,m.
     
    376364   
    377365interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     366
     367
     368lemma vsplit_ok:
     369  ∀A: Type[0].
     370  ∀m, n: nat.
     371  ∀v: Vector A (m + n).
     372  ∀upper: Vector A m.
     373  ∀lower: Vector A n.
     374    〈upper, lower〉 = vsplit A m n v →
     375      upper @@ lower = v.
     376  #A #m #n #v #upper #lower
     377  cases daemon
     378qed.
    378379
    379380lemma vector_append_zero:
Note: See TracChangeset for help on using the changeset viewer.