Changeset 998 for src/ASM/Vector.ma
 Timestamp:
 Jun 20, 2011, 5:05:23 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r961 r998 170 170 split' A m n v. 171 171 172 173 172 definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝ 174 173 λA: Type[0]. … … 306 305 307 306 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 307 308 axiom split_elim': 309 ∀A: Type[0]. 310 ∀B: Type[1]. 311 ∀l, m, v. 312 ∀T: Vector A l → Vector A m → B. 313 ∀P: B → Prop. 314 (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) → 315 P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt). 316 317 axiom split_elim'': 318 ∀A: Type[0]. 319 ∀B,B': Type[1]. 320 ∀l, m, v. 321 ∀T: Vector A l → Vector A m → B. 322 ∀T': Vector A l → Vector A m → B'. 323 ∀P: B → B' → Prop. 324 (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) → 325 P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt) 326 (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt). 308 327 309 328 let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
Note: See TracChangeset
for help on using the changeset viewer.