idris-0.9.16: test/tutorial006/tutorial006a.idr
import Data.Vect vapp : Vect n a -> Vect m a -> Vect (n + m) a vapp Nil ys = ys vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
import Data.Vect vapp : Vect n a -> Vect m a -> Vect (n + m) a vapp Nil ys = ys vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN