The type Vector
represents lists with fixed length.
Equations
- Vector.instDecidableEqVector = inferInstanceAs (DecidableEq { l // List.length l = n })
The empty vector with elements of type α
Equations
- Vector.nil = { val := [], property := (_ : List.length [] = List.length []) }
If a : α
and l : Vector α n
, then cons a l
, is the vector of length n + 1
whose first element is a and with l as the rest of the list.
Equations
- Vector.cons x x = match x, x with | a, { val := v, property := h } => { val := a :: v, property := (_ : Nat.succ (List.length v) = Nat.succ n) }
The length of a vector.
Equations
- Vector.length x = n
The first element of a vector with length at least 1
.
Equations
- Vector.head x = match x with | { val := [], property := h } => Nat.noConfusion h | { val := a :: tail, property := property } => a
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.
The list obtained from a vector.
Equations
- Vector.toList v = v.val
nth element of a vector, indexed by a Fin
type.
Equations
- Vector.get x x = match x, x with | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l)
Appending a vector to another.
Equations
- Vector.append x x = match x, x with | { val := l₁, property := h₁ }, { val := l₂, property := h₂ } => { val := l₁ ++ l₂, property := (_ : List.length (l₁ ++ l₂) = n + m) }
Elimination rule for Vector
.
Equations
- Vector.elim H x = match x with | { val := l, property := h } => match n, h with | .(List.length l), (_ : List.length l = List.length l) => H l
Map a vector under a function.
Equations
- Vector.map f x = match x with | { val := l, property := h } => { val := List.map f l, property := (_ : List.length (List.map f l) = n) }
Vector obtained by repeating an element.
Equations
- Vector.replicate n a = { val := List.replicate n a, property := (_ : List.length (List.replicate n a) = n) }
Take i
elements from a vector of length n
; we can have i > n
.
Equations
- Vector.take i x = match x with | { val := l, property := p } => { val := List.take i l, property := (_ : List.length (List.take i l) = min i n) }
Remove the element at position i
from a vector of length n
.
Equations
- Vector.removeNth i x = match x with | { val := l, property := p } => { val := List.removeNth l ↑i, property := (_ : List.length (List.removeNth l ↑i) = n - 1) }
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))
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.