concat-3.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 concat : Vect n a 
            -> Vect m a 
            -> Vect (m + n) a
concat {a=a} {m=m} {n=n} (x :: xs) ys = replace {P = \k => Vect k a} (sPlusAssoc m n) (x :: concat xs ys)
concat Nil       ys = replace sPlusAssoc $ ys

gistfile1.txt

- + Errors (1)
 `-- tutorial.idr line 18 col 8:
     When elaborating left hand side of snoc.concat:
     When elaborating an application of snoc.concat:
             Can't unify
                     Vect (S n1) a
             with
                     Vect n a
             
             Specifically:
                     Can't unify
                             S n1
                     with
                             n