Vector Basics

This module defines some basic vector functions - where basic really just means pure vector functions which do not require any other datatype. There is currently only one theorem vect_nth_append: Given two vectors t and s with dimensions m and n, respectively, retrieving the xth element in s with $x\in\{0,\ldots,n-1\}$ is equivalent to retrieving the xth element in $\texttt{vappend}\ t\ s$.

 ** Module lib_vectors_basics Imports lib_vectors
  vsingleton = ... : {T|Type}T->vect T one
  vappend = ... :
    {m,n|nat}{T|Type}(vect T m)->(vect T n)->vect T (plus m n)
  vtack = ... : {m|nat}{T|Type}T->(vect T m)->vect T (suc m)
  vect_nth_append = ... :
    {T|Type}{n|nat}{x:fin n}{s:vect T n}{m|nat}{t:vect T m}
    Eq (vect_nth (f_plus x) (vappend t s)) (vect_nth x s)