Changeset 2122 for src/ASM/Vector.ma
 Timestamp:
 Jun 27, 2012, 3:36:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r2121 r2122 222 222 let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝ 223 223 vsplit' A m n v. 224 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. 224 236 225 237 lemma vsplit_zero:
Note: See TracChangeset
for help on using the changeset viewer.