ivor-0.1.5: examplett/vec.tt

Load "nat.tt";

Data Vect (A:*) : (n:Nat)* =
   Vnil : (Vect A O)
 | Vcons : (k:Nat)(a:A)(v:Vect A k)(Vect A (S k));

vec_append : (A:*)(m,n:Nat)(xs:Vect A m)(ys:Vect A n)(Vect A (plus m n));
intros;
induction xs;
fill ys;
intros;
fill (Vcons _ _ a v_IH);
Qed;