app : Vect n a -> Vect m a -> Vect (n + m) a is a type signature for a function, `app`, which should append a vector (`Vect`) of length `n` to a vector of leng

app : Vect n a -> Vect m a -> Vect (n + m) a is a type signature for a function, `app`, which should append a vector (`Vect`) of length `n` to a vector of length `m`. What's cool about Idris and other dependently-typed languages is that the length of the resulting vector, `n + m`, can be tracked in the type. This can prevent a whole slew of errors.