[andrus]

    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.