snoc-error

- + Errors (1)
 `-- tutorial.idr line 41 col 5:
     When elaborating right hand side of snoc:
     Can't unify
             Vect (n + 1) a
     with
             Vect (S n) a
     
     Specifically:
             Can't unify
                     plus n 1
             with
                     S n

snoc.idr

append : Vect n a -> Vect m a -> Vect (n + m) a 
append (x :: Nil) ys = x :: ys
append (x :: xs)  ys = x :: (append xs ys)

snoc : Vect n a -> a -> Vect (S n) a
snoc xs a =  append xs (a :: Nil)