Changeset 873


Ignore:
Timestamp:
Jun 2, 2011, 5:47:00 PM (8 years ago)
Author:
sacerdot
Message:

Script improved. Maybe this requires an svn up of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r854 r873  
    117117    /2/;
    118118qed.
    119    
     119
    120120let rec set_index_weak (A: Type[0]) (n: nat)
    121121                       (v: Vector A n) (m: nat) (a: A) on m ≝
     
    457457  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
    458458  ] 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 //
     460qed.
    466461
    467462lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
Note: See TracChangeset for help on using the changeset viewer.