concat.idr

-- proving that these are equivalent
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


-- want to use the proof here
total concat : Vect n a -> Vect m a -> Vect (m + n) a
concat (x :: xs) ys = x :: (concat xs ys)
concat Nil ys = ys

current-error

 + Errors (1)
 `-- tutorial.idr line 15 col 8:
     When elaborating right hand side of snoc.concat:
     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)