Definitions on Arrays #
This file contains various definitions on Array
. It does not contain
proofs about these definitions, those are contained in other files in Batteries.Data.Array
.
Check whether xs
and ys
are equal as sets, i.e. they contain the same
elements when disregarding order and duplicates. O(n*m)
! If your element type
has an Ord
instance, it is asymptotically more efficient to sort the two
arrays, remove duplicates and then compare them elementwise.
Equations
Instances For
Returns the first minimal element among d
and elements of the array.
If start
and stop
are given, only the subarray xs[start:stop]
is
considered (in addition to d
).
Equations
- xs.minWith d start stop = Array.foldl (fun (min x : α) => if (compare x min).isLT = true then x else min) d xs start stop
Instances For
Find the first minimal element of an array. If the array is empty, d
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
Instances For
Find the first minimal element of an array. If the array is empty, none
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
Instances For
Find the first minimal element of an array. If the array is empty, default
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
- xs.minI start stop = xs.minD default start stop
Instances For
Returns the first maximal element among d
and elements of the array.
If start
and stop
are given, only the subarray xs[start:stop]
is
considered (in addition to d
).
Equations
- xs.maxWith d start stop = xs.minWith d start stop
Instances For
Find the first maximal element of an array. If the array is empty, d
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
- xs.maxD d start stop = xs.minD d start stop
Instances For
Find the first maximal element of an array. If the array is empty, none
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
- xs.max? start stop = xs.min? start stop
Instances For
Find the first maximal element of an array. If the array is empty, default
is
returned. If start
and stop
are given, only the subarray xs[start:stop]
is
considered.
Equations
- xs.maxI start stop = xs.minI start stop
Instances For
Alias of Array.flatten
.
Joins array of array into a single array.
flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]
= #[a₁, a₂, ⋯, b₁, b₂, ⋯]
Equations
Instances For
Safe Nat Indexed Array functions #
The functions in this section offer variants of Array functions which use Nat
indices
instead of Fin
indices. All these functions have as parameter a proof that the index is
valid for the array. But this parameter has a default argument by get_elem_tactic
which
should prove the index bound.
setN a i h x
sets an element in a vector using a Nat index which is provably valid.
A proof by get_elem_tactic
is provided as a default argument for h
.
This will perform the update destructively provided that a
has a reference count of 1 when called.
Equations
- a.setN i x h = a.set ⟨i, h⟩ x
Instances For
swapN a i j hi hj
swaps two Nat
indexed entries in an Array α
.
Uses get_elem_tactic
to supply a proof that the indices are in range.
hi
and hj
are both given a default argument by get_elem_tactic
.
This will perform the update destructively provided that a
has a reference count of 1 when called.
Equations
- a.swapN i j hi hj = a.swap ⟨i, hi⟩ ⟨j, hj⟩
Instances For
swapAtN a i h x
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 proof of i < a.size
with get_elem_tactic
where feasible.
Equations
- a.swapAtN i x h = a.swapAt ⟨i, h⟩ x
Instances For
eraseIdxN a i h
Removes the element at position i
from a vector of length n
.
h : i < a.size
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
- a.eraseIdxN i h = a.feraseIdx ⟨i, h⟩
Instances For
finRange n
is the array of all elements of Fin n
in order.
Equations
- Array.finRange n = Array.ofFn fun (i : Fin n) => i
Instances For
Check whether a subarray contains an element.
Equations
- as.contains a = Subarray.any (fun (x : α) => x == a) as