Changeset 2122 for src/ASM/Vector.ma


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

More stuff moved around in proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r2121 r2122  
    222222let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
    223223 vsplit' A m n v.
     224
     225lemma 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
     235qed.
    224236
    225237lemma vsplit_zero:
Note: See TracChangeset for help on using the changeset viewer.