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)