|
|
|
|
|
|
by andrus
3821 days ago
|
|
|
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. |
|
|