Vectors #
Vector α n
is an array with a statically fixed size n
.
It combines the benefits of Lean's special support for Arrays
that offer O(1)
accesses and in-place mutations for arrays with no more than one reference,
with static guarantees about the size of the underlying array.
Equations
- Batteries.instReprVector = { reprPrec := Batteries.reprVector✝ }
Equations
- Batteries.instDecidableEqVector = Batteries.decEqVector✝
Syntax for Vector α n
Equations
- One or more equations did not get rendered due to their size.
Instances For
Custom eliminator for Vector α n
through Array α
Equations
- Batteries.Vector.elimAsArray mk { toArray := a, size_eq := ⋯ } = mk a
Instances For
Custom eliminator for Vector α n
through List α
Equations
- Batteries.Vector.elimAsList mk { toArray := { toList := a }, size_eq := ⋯ } = mk a
Instances For
Vector.empty
produces an empty vector
Equations
- Batteries.Vector.empty = { toArray := #[], size_eq := ⋯ }
Instances For
Make an empty vector with pre-allocated capacity
Equations
- Batteries.Vector.mkEmpty capacity = { toArray := Array.mkEmpty capacity, size_eq := ⋯ }
Instances For
Makes a vector of size n
with all cells containing v
Equations
- Batteries.Vector.mkVector n v = { toArray := mkArray n v, size_eq := ⋯ }
Instances For
Returns a vector of size 1
with a single element v
Equations
Instances For
The Inhabited instance for Vector α n
with [Inhabited α]
produces a vector of size n
with all its elements equal to the default
element of type α
Equations
- Batteries.Vector.instInhabited = { default := Batteries.Vector.mkVector n default }
nth element of a vector, indexed by a Fin
type.
Instances For
Vector lookup function that takes an index i
of type USize
Equations
- v.uget i h = v.toArray.uget i ⋯
Instances For
Vector α n
instance for the GetElem
typeclass.
Equations
- Batteries.Vector.instGetElemNatLt = { getElem := fun (x : Batteries.Vector α n) (i : Nat) (h : i < n) => x.get ⟨i, h⟩ }
v.back! v
gets the last element of the vector.
panics if v
is empty.
Instances For
v.back?
gets the last element x
of the array as some x
if it exists. Else the vector is empty and it returns none
Instances For
push v x
pushes x
to the end of vector v
in O(1) time
Equations
- Batteries.Vector.push x v = { toArray := v.toArray.push x, size_eq := ⋯ }
Instances For
pop v
returns the vector with the last element removed
Equations
- v.pop = { toArray := v.toArray.pop, size_eq := ⋯ }
Instances For
Sets an element in a vector using a Fin index.
This will perform the update destructively provided that a has a reference count of 1 when called.
Instances For
setN v i h x
sets an element in a vector using a Nat index which is provably valid.
By default a proof by get_elem_tactic
is provided.
This will perform the update destructively provided that a has a reference count of 1 when called.
Equations
- v.setN i x h = v.set ⟨i, h⟩ x
Instances For
Sets an element in a vector, or do nothing if the index is out of bounds.
This will perform the update destructively provided that a has a reference count of 1 when called.
Equations
- v.setD i x = { toArray := v.toArray.setD i x, size_eq := ⋯ }
Instances For
Sets an element in an array, or panic if the index is out of bounds.
This will perform the update destructively provided that a has a reference count of 1 when called.
Equations
- v.set! i x = { toArray := v.toArray.set! i x, size_eq := ⋯ }
Instances For
Appends a vector to another.
Equations
Instances For
Equations
- Batteries.Vector.instHAppendHAddNat = { hAppend := Batteries.Vector.append }
Creates a vector from another with a provably equal length.
Equations
- Batteries.Vector.cast h { toArray := x_1, size_eq := p } = { toArray := x_1, size_eq := ⋯ }
Instances For
extract v start halt
Returns the slice of v
from indices start
to stop
(exclusive).
If start
is greater or equal to stop
, the result is empty.
If stop
is greater than the size of v
, the size is used instead.
Equations
- v.extract start stop = { toArray := v.toArray.extract start stop, size_eq := ⋯ }
Instances For
Maps a vector under a function.
Equations
- Batteries.Vector.map f v = { toArray := Array.map f v.toArray, size_eq := ⋯ }
Instances For
Maps two vectors under a curried function of two variables.
Equations
- { toArray := a, size_eq := h₁ }.zipWith { toArray := b, size_eq := h₂ } x = { toArray := a.zipWith b x, size_eq := ⋯ }
Instances For
Returns a vector of length n
from a function on Fin n
.
Equations
- Batteries.Vector.ofFn f = { toArray := Array.ofFn f, size_eq := ⋯ }
Instances For
Swaps two entries in a Vector.
This will perform the update destructively provided that v
has a reference count of 1 when called.
Instances For
swapN v i j hi hj
swaps two Nat
indexed entries in a Vector α n
.
Uses get_elem_tactic
to supply proofs hi
and hj
respectively
that the indices i
and j
are in range.
This will perform the update destructively provided that v
has a reference count of 1 when called.
Equations
- v.swapN i j hi hj = v.swap ⟨i, hi⟩ ⟨j, hj⟩
Instances For
Swaps two entries in a Vector α n
, or panics if either index is out of bounds.
This will perform the update destructively provided that v
has a reference count of 1 when called.
Equations
- v.swap! i j = { toArray := v.toArray.swap! i j, size_eq := ⋯ }
Instances For
Swaps the entry with index i : Fin n
in the vector for a new entry.
The old entry is returned with the modified vector.
Equations
Instances For
Swaps the entry with index i : Nat
in the vector for a new entry x
.
The old entry is returned alongwith the modified vector.
Automatically generates a proof of i < n
with get_elem_tactic
where feasible.
Equations
- v.swapAtN i x h = v.swapAt ⟨i, h⟩ x
Instances For
swapAt! v i x
swaps out the entry at index i : Nat
in the vector for x
, if the index is valid.
Otherwise it panics The old entry is returned with the modified vector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
range n
returns the vector #v[0,1,2,...,n-1]
.
Equations
- Batteries.Vector.range n = { toArray := Array.range n, size_eq := ⋯ }
Instances For
shrink v m
shrinks the vector to the first m
elements if m < n
.
Returns v
unchanged if m ≥ n
.
Equations
- v.shrink m = { toArray := v.toArray.shrink m, size_eq := ⋯ }
Instances For
Drops the first (up to) i
elements from a vector of length n
.
If m ≥ n
, the return value is empty.
Equations
- Batteries.Vector.drop i v = Batteries.Vector.cast ⋯ (v.extract i n)
Instances For
Takes the first (up to) i
elements from a vector of length n
.
Instances For
isEqv
takes a given boolean property p
. It returns true
if and only if p a[i] b[i]
holds true for all valid indices i
.
Equations
- a.isEqv b p = a.toArray.isEqvAux b.toArray ⋯ p 0 ⋯
Instances For
Equations
- Batteries.Vector.instBEq = { beq := fun (a b : Batteries.Vector α n) => a.isEqv b BEq.beq }
reverse v
reverses the vector v
.
Equations
- v.reverse = { toArray := v.toArray.reverse, size_eq := ⋯ }
Instances For
O(|v| - i)
. feraseIdx v i
removes the element at position i
in vector v
.
Instances For
Vector.tail
produces the tail of the vector v
.
Instances For
O(|v| - i)
. eraseIdx! v i
removes the element at position i
from vector v
of length n
.
Panics if i
is not less than n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
eraseIdxN v i h
removes the element at position i
from a vector of length n
.
h : i < n
has a default argument by get_elem_tactic
which tries to supply a proof
that the index is valid.
This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.
Equations
- v.eraseIdxN i h = v.feraseIdx ⟨i, h⟩
Instances For
If x
is an element of vector v
at index j
, then indexOf? v x
returns some j
.
Otherwise it returns none
.
Equations
Instances For
isPrefixOf as bs
returns true iff vector as
is a prefix of vectorbs
Equations
- as.isPrefixOf bs = as.toArray.isPrefixOf bs.toArray