prepend-err

- tutorial.idr line 16 col 9:
     When elaborating right hand side of prepend:
     Can't unify
             Vect (S (m + n)) a
     with
             Vect (plus m (S n)) a
     
     Specifically:
             Can't unify
                     S (m + n)
             with
                     plus m (S n)

prepend.idr

sPlusAssoc : (m, n: Nat) -> S (m + n) = plus m (S n)
sPlusAssoc Z n = refl
sPlusAssoc (S m) n = rewrite sPlusAssoc m n in refl
 
total prepend : Vect n a -> Vect m a -> Vect (m + n) a
prepend (x :: xs) ys = x :: (prepend xs ys)
prepend Nil       ys = ys