The type Vector
represents lists with fixed length.
Vector α n
is the type of lists of length n
with elements of type α
.
Equations
- Mathlib.Vector α n = { l : List α // l.length = n }
Instances For
Equations
- Mathlib.Vector.instDecidableEq = inferInstanceAs (DecidableEq { l : List α // l.length = n })
The empty vector with elements of type α
Equations
- Mathlib.Vector.nil = ⟨[], ⋯⟩
Instances For
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
- Mathlib.Vector.cons x✝ x = match x✝, x with | a, ⟨v, h⟩ => ⟨a :: v, ⋯⟩
Instances For
The first element of a vector with length at least 1
.
Instances For
The head of a vector obtained by prepending is the element prepended.
The tail of a vector, with an empty vector having empty tail.
Instances For
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.
nth element of a vector, indexed by a Fin
type.
Instances For
Appending a vector to another.
Instances For
Elimination rule for Vector
.
Equations
- Mathlib.Vector.elim H x = match x with | ⟨l, h⟩ => match n, h with | .(l.length), ⋯ => H l
Instances For
Map a vector under a function.
Equations
- Mathlib.Vector.map f x = match x with | ⟨l, h⟩ => ⟨List.map f l, ⋯⟩
Instances For
Mapping two vectors under a curried function of two variables.
Equations
- Mathlib.Vector.map₂ f x✝ x = match x✝, x with | ⟨x, property⟩, ⟨y, property_1⟩ => ⟨List.zipWith f x y, ⋯⟩
Instances For
Vector obtained by repeating an element.
Equations
- Mathlib.Vector.replicate n a = ⟨List.replicate n a, ⋯⟩
Instances For
Drop i
elements from a vector of length n
; we can have i > n
.
Equations
- Mathlib.Vector.drop i x = match x with | ⟨l, p⟩ => ⟨List.drop i l, ⋯⟩
Instances For
Take i
elements from a vector of length n
; we can have i > n
.
Equations
- Mathlib.Vector.take i x = match x with | ⟨l, p⟩ => ⟨List.take i l, ⋯⟩
Instances For
Remove the element at position i
from a vector of length n
.
Equations
- Mathlib.Vector.eraseIdx i x = match x with | ⟨l, p⟩ => ⟨l.eraseIdx ↑i, ⋯⟩
Instances For
Alias of Mathlib.Vector.eraseIdx
.
Remove the element at position i
from a vector of length n
.
Instances For
Vector of length n
from a function on Fin n
.
Equations
- Mathlib.Vector.ofFn x_2 = Mathlib.Vector.nil
- Mathlib.Vector.ofFn f = Mathlib.Vector.cons (f 0) (Mathlib.Vector.ofFn fun (i : Fin n) => f i.succ)
Instances For
Create a vector from another with a provably equal length.
Equations
- Mathlib.Vector.congr h x = match x with | ⟨x, p⟩ => ⟨x, ⋯⟩
Instances For
Runs a function over a vector returning the intermediate results and a final result.
Equations
- Mathlib.Vector.mapAccumr f x✝ x = match x✝, x with | ⟨x, px⟩, c => let res := List.mapAccumr f x c; (res.fst, ⟨res.snd, ⋯⟩)
Instances For
Runs a function over a pair of vectors returning the intermediate results and a final result.
Equations
- Mathlib.Vector.mapAccumr₂ f x✝¹ x✝ x = match x✝¹, x✝, x with | ⟨x, px⟩, ⟨y, py⟩, c => let res := List.mapAccumr₂ f x y c; (res.fst, ⟨res.snd, ⋯⟩)
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
- v.shiftLeftFill i fill = Mathlib.Vector.congr ⋯ ((Mathlib.Vector.drop i v).append (Mathlib.Vector.replicate (min n i) 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
.
Equations
- v.shiftRightFill i fill = Mathlib.Vector.congr ⋯ ((Mathlib.Vector.replicate (min n i) fill).append (Mathlib.Vector.take (n - i) v))
Instances For
Basic Theorems #
Vector is determined by the underlying list.
A vector of length 0
is a nil
vector.
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.
Equations
- Mathlib.Vector.instGetElemNatLt = { getElem := fun (x : Mathlib.Vector α n) (i : ℕ) (h : i < n) => x.get ⟨i, h⟩ }