//@ consumes the vector `v`. The caller hence loses access to its vector. However, there is something
//@ we can do if we don't want that to happen: We can explicitly `clone` the vector,
//@ which means that a full (or *deep*) copy will be performed. Technically,
//@ consumes the vector `v`. The caller hence loses access to its vector. However, there is something
//@ we can do if we don't want that to happen: We can explicitly `clone` the vector,
//@ which means that a full (or *deep*) copy will be performed. Technically,