on ddfdb2e help sign in
Idris-dev/test/tutorial006/tutorial006a.idr
5 lines 117 B history raw
1vapp : Vect n a -> Vect m a -> Vect (n + m) a
2vapp Nil ys = ys
3vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN