The type List.Vector
represents lists with fixed length.
TODO: The API of List.Vector
is quite incomplete relative to Vector
,
and in particular does not use x[i]
(that is GetElem
notation) as the preferred accessor.
Any combination of reducing the use of List.Vector
in Mathlib, or modernising its API,
would be welcome.
List.Vector α n
is the type of lists of length n
with elements of type α
.
Note that there is also Vector α n
in the root namespace,
which is the type of arrays of length n
with elements of type α
.
Typically, if you are doing programming or verification, you will primarily use Vector α n
,
and if you are doing mathematics, you may want to use List.Vector α n
instead.
Equations
Instances For
Equations
The empty vector with elements of type α
Equations
Instances For
Vector obtained by repeating an element.
Equations
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
.
Equations
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
.