The type Vector
represents lists with fixed length.
The empty vector with elements of type α
Instances For
The head of a vector obtained by prepending is the element prepended.
The tail of a vector obtained by prepending is the vector prepended. to
Prepending the head of a vector to its tail gives the vector.
Elimination rule for Vector
.
Instances For
Vector obtained by repeating an element.
Instances For
Vector of length n
from a function on Fin n
.
Equations
- Vector.ofFn x_2 = Vector.nil
- Vector.ofFn f = Vector.cons (f 0) (Vector.ofFn fun i => f (Fin.succ i))
Instances For
Shift Primitives #
shiftLeftFill v i
is the vector obtained by left-shifting v
i
times and padding with the
fill
argument. If v.length < i
then this will return replicate n fill
.
Instances For
shiftRightFill v i
is the vector obtained by right-shifting v
i
times and padding with the
fill
argument. If v.length < i
then this will return replicate n fill
.
Instances For
Basic Theorems #
Vector is determined by the underlying list.
Vector of length from a list v
with witness that v
has length n
maps to v
under toList
.
A nil vector maps to a nil list.
The length of the list to which a vector of length n
maps is n
.
toList
of cons
of a vector and an element is
the cons
of the list obtained by toList
and the element
Appending of vectors corresponds under toList
to appending of lists.