next up previous contents
Next: Quotient Types Up: Vectors Previous: Vector Definitions

Vector Basics

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)



Lego
Fri May 24 19:01:27 BST 1996