Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

14 lines (11 sloc) 0.261 kb
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;
Jump to Line
Something went wrong with that request. Please try again.