- Timestamp:
- Jun 2, 2011, 5:47:00 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Vector.ma
r854 r873 117 117 /2/; 118 118 qed. 119 119 120 120 let rec set_index_weak (A: Type[0]) (n: nat) 121 121 (v: Vector A n) (m: nat) (a: A) on m ≝ … … 457 457 | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 458 458 ] P v. 459 @(λA,n. λP:Vector A n → Type[0]. λv. match v return 460 ? 461 with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P) 462 [ // | // ] qed. 463 (* XXX Proof below fails at qed. 464 #A #n #P * [ #H @H | #m #h #t #H @H ] qed. 465 *) 459 #A #n #P #v generalize in match P cases v normalize // 460 qed. 466 461 467 462 lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
Note: See TracChangeset
for help on using the changeset viewer.