This modue defines some basic vector functions - where basic really just means pure vector functions which do not require any other datatype. No theorems have been provided yet.
** Module lib_vectors_basics Imports lib_vectors
* vsingleton = ... : {T|SET}T->vect T one
* vappend = ... :
{m,n|nat}{T|SET}(vect T m)->(vect T n)->vect T (plus m n)
* vtack = ... : {m|nat}{T|SET}T->(vect T m)->vect T (suc m)