Arrays can be vastly more efficient than lists or other sequences in compiled code.
In part, this is because they offer good locality: because all the elements of the sequence are next to each other in memory, the processor's caches can be used efficiently.
Even more importantly, if there is only a single reference to an array, operations that might otherwise copy or allocate a data structure can be implemented via mutation.
Lean code that uses an array in such a way that there's only ever one unique reference (that is, uses it linearly) avoids the performance overhead of persistent data structures while still being as convenient to write, read, and prove things about as ordinary pure functional programs.
Arrayα is the type of dynamic arrays with elements
from α. This type has special support in the runtime.
Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed destructively. This results in performance comparable to mutable
arrays in imperative programming languages.
An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
Array.size, but the capacity is not observable from Lean code. Array.emptyWithCapacityn creates
an array which is equal to #[], but internally allocates an array of capacity n. When the size
exceeds the capacity, allocation is required to grow the array.
From the point of view of proofs, Arrayα is just a wrapper around Listα.
Converts an Arrayα into a Listα that contains the same elements in the same order.
At runtime, this is implemented by Array.toListImpl and is O(n) in the length of the
array.
The logical model of arrays is a structure that contains a single field, which is a list of elements.
This is convenient when specifying and proving properties of array-processing functions at a low level.
Lean's arrays are dynamic arrays, which are blocks of continuous memory with a defined capacity, not all of which is typically in use.
As long as the number of elements in the array is less than the capacity, new items can be added to the end without reallocating or moving the data.
Adding items to an array that has no extra space results in a reallocation that doubles the capacity.
The amortized overhead scales linearly with the size of the array.
The values in the array are represented as described in the section on the foreign function interface.
Memory layout of arrays
After the object header, an array contains:
size
The number of objects currently stored in the array
capacity
The number of objects that fit in the memory allocated for the array
data
The values in the array
Many array functions in the Lean runtime check whether they have exclusive access to their argument by consulting the reference count in the object header.
If they do, and the array's capacity is sufficient, then the existing array can be mutated rather than allocating fresh memory.
Otherwise, a new array must be allocated.
Despite the fact that they appear to be an ordinary constructor and projection, Array.mk and Array.toList take time linear in the size of the array in compiled code.
This is because converting between linked lists and packed arrays must necessarily visit each element.
Mutable arrays can be used to write very efficient code.
However, they are a poor persistent data structure.
Updating a shared array rules out mutation, and requires time linear in the size of the array.
When using arrays in performance-critical code, it's important to ensure that they are used linearly.
Array literals allow arrays to be written directly in code.
They may be used in expression or pattern contexts.
syntaxArray Literals
Array literals begin with #[ and contain a comma-separated sequence of terms, terminating with ].
term::= ...
|Syntax for `Array α`.
Conventions for notations in identifiers:
* The recommended spelling of `#[]` in identifiers is `empty`.
* The recommended spelling of `#[x]` in identifiers is `singleton`.#[term,*]
Array Literals
Array literals may be used as expressions or as patterns.
This is a cached value, so it is O(1) to access. The space allocated for an array, referred to as
its capacity, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
Returns the size of the array as a platform-native unsigned integer.
This is a low-level version of Array.size that directly queries the runtime system's
representation of arrays. While this is not provable, Array.usize always returns the exact size of
the array since the implementation only supports arrays of size less than USize.size.
Returns the index of the first element equal to a, or the size of the array if no element is equal
to a. The index is returned as a Fin, which guarantees that it is in bounds.
Returns a subarray of an array, with the given bounds.
If start or stop are not valid bounds for a subarray, then they are clamped to array's size.
Additionally, the starting index is clamped to the ending index.
Array.push.{u} {α : Type u} (a : Arrayα) (v : α) : Arrayα
Array.push.{u} {α : Type u} (a : Arrayα)
(v : α) : Arrayα
Adds an element to the end of an array. The resulting array's size is one greater than the input
array. If there are no other references to the array, then it is modified in-place.
This takes amortized O(1) time because Arrayα is represented by a dynamic array.
Removes the last element of an array. If the array is empty, then it is returned unmodified. The
modification is performed in-place when the reference to the array is unique.
Array.swapIfInBounds.{u} {α : Type u} (xs : Arrayα) (i j : Nat) :
Arrayα
Array.swapIfInBounds.{u} {α : Type u}
(xs : Arrayα) (i j : Nat) : Arrayα
Swaps two elements of an array, returning the array unchanged if either index is out of bounds. The
modification is performed in-place when the reference to the array is unique.
Array.replace.{u} {α : Type u} [BEqα] (xs : Arrayα) (a b : α) :
Arrayα
Array.replace.{u} {α : Type u} [BEqα]
(xs : Arrayα) (a b : α) : Arrayα
Replaces the first occurrence of a with b in an array. The modification is performed in-place
when the reference to the array is unique. Returns the array unmodified when a is not present.
Array.set.{u_1} {α : Type u_1} (xs : Arrayα) (i : Nat) (v : α)
(h : i < xs.size := by get_elem_tactic) : Arrayα
Array.set.{u_1} {α : Type u_1}
(xs : Arrayα) (i : Nat) (v : α)
(h : i < xs.size := by
get_elem_tactic) :
Arrayα
Replaces the element at a given index in an array.
No bounds check is performed, but the function requires a proof that the index is in bounds. This
proof can usually be omitted, and will be synthesized automatically.
The array is modified in-place if there are no other references to it.
Array.modifyM.{u, u_1} {α : Type u} {m : Type u → Type u_1} [Monadm]
(xs : Arrayα) (i : Nat) (f : α → mα) : m (Arrayα)
Array.modifyM.{u, u_1} {α : Type u}
{m : Type u → Type u_1} [Monadm]
(xs : Arrayα) (i : Nat) (f : α → mα) :
m (Arrayα)
Replaces the element at the given index, if it exists, with the result of applying the monadic
function f to it. If the index is invalid, the array is returned unmodified and f is not called.
Examples:
#[1, 2, 30, 4]It was 3
#eval#[1,2,3,4].modifyM2funx=>doIO.printlns!"It was {x}"returnx*10Itwas3#[1,2,30,4]#[1, 2, 3, 4]#eval#[1,2,3,4].modifyM6funx=>doIO.printlns!"It was {x}"returnx*10#[1,2,3,4]
Array.insertIdx!.{u} {α : Type u} (as : Arrayα) (i : Nat) (a : α) :
Arrayα
Array.insertIdx!.{u} {α : Type u}
(as : Arrayα) (i : Nat) (a : α) :
Arrayα
Inserts an element into an array at the specified index. Panics if the index is greater than the
size of the array.
In other words, the new element is inserted into the array as after the first i elements of
as.
This function takes worst case O(n) time because it has to swap the inserted element into place.
Array.insertIdx and Array.insertIdxIfInBounds are safer alternatives.
Returns the first n elements of an array. The resulting array is produced by repeatedly calling
Array.pop. If n is greater than the size of the array, it is returned unmodified.
If the reference to the array is unique, then this function uses in-place modification.
The optional parameter lt specifies an ordering predicate. It defaults to LT.lt, which must be
decidable to be used for sorting. Use Array.qsortOrd to sort the array according to the Ordα
instance.
The optional parameters low and high delimit the region of the array that is sorted. Both are
inclusive, and default to sorting the entire array.
Array.binInsertM.{u, v} {α : Type u} {m : Type u → Type v} [Monadm]
(lt : α → α → Bool) (merge : α → mα) (add : Unit → mα)
(as : Arrayα) (k : α) : m (Arrayα)
Array.binInsertM.{u, v} {α : Type u}
{m : Type u → Type v} [Monadm]
(lt : α → α → Bool) (merge : α → mα)
(add : Unit → mα) (as : Arrayα)
(k : α) : m (Arrayα)
Inserts an element k into a sorted array as such that the resulting array is sorted.
The ordering predicate lt should be a total order on elements, and the array as should be sorted
with respect to lt.
If an element that lt equates to k is already present in as, then merge is applied to the
existing element to determine the value of that position in the resulting array. If no element equal
to k is present, then add is used to determine the value to be inserted.
Binary search for an element equivalent to k in the sorted array as. Returns the element from
the array, if it is found, or none otherwise.
The array as must be sorted according to the comparison operator lt, which should be a total
order.
The optional parameters lo and hi determine the region of the array indices to be searched. Both
are inclusive, and default to searching the entire array.
Binary search for an element equivalent to k in the sorted array as. Returns true if the
element is found, or false otherwise.
The array as must be sorted according to the comparison operator lt, which should be a total
order.
The optional parameters lo and hi determine the region of the array indices to be searched. Both
are inclusive, and default to searching the entire array.
Folds a function over an array from the right, accumulating a value starting with init. The
accumulated value is combined with the each element of the array in reverse order, using f.
The optional parameters start and stop control the region of the array to be folded. Folding
proceeds from start (exclusive) to stop (inclusive), so no folding occurs unless start>stop.
By default, the entire array is used.
Array.foldrM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w}
[Monadm] (f : α → β → mβ) (init : β) (as : Arrayα)
(start : Nat := as.size) (stop : Nat := 0) : mβ
Array.foldrM.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : α → β → mβ) (init : β)
(as : Arrayα) (start : Nat := as.size)
(stop : Nat := 0) : mβ
Folds a monadic function over an array from the right, accumulating a value starting with init.
The accumulated value is combined with the each element of the list in reverse order, using f.
The optional parameters start and stop control the region of the array to be folded. Folding
proceeds from start (exclusive) to stop (inclusive), so no folding occurs unless start>stop.
By default, the entire array is folded.
Folds a function over an array from the left, accumulating a value starting with init. The
accumulated value is combined with the each element of the array in order, using f.
The optional parameters start and stop control the region of the array to be folded. Folding
proceeds from start (inclusive) to stop (exclusive), so no folding occurs unless start<stop.
By default, the entire array is used.
Array.foldlM.{u, v, w} {α : Type u} {β : Type v} {m : Type v → Type w}
[Monadm] (f : β → α → mβ) (init : β) (as : Arrayα)
(start : Nat := 0) (stop : Nat := as.size) : mβ
Array.foldlM.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : β → α → mβ) (init : β)
(as : Arrayα) (start : Nat := 0)
(stop : Nat := as.size) : mβ
Folds a monadic function over a list from the left, accumulating a value starting with init. The
accumulated value is combined with the each element of the list in order, using f.
The optional parameters start and stop control the region of the array to be folded. Folding
proceeds from start (inclusive) to stop (exclusive), so no folding occurs unless start<stop.
By default, the entire array is folded.
Array.forM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monadm]
(f : α → mPUnit) (as : Arrayα) (start : Nat := 0)
(stop : Nat := as.size) : mPUnit
Array.forM.{u, v, w} {α : Type u}
{m : Type v → Type w} [Monadm]
(f : α → mPUnit) (as : Arrayα)
(start : Nat := 0)
(stop : Nat := as.size) : mPUnit
Applies the monadic action f to each element of an array, in order.
The optional parameters start and stop control the region of the array to which f should be
applied. Iteration proceeds from start (inclusive) to stop (exclusive), so f is not invoked
unless start<stop. By default, the entire array is used.
Array.forRevM.{u, v, w} {α : Type u} {m : Type v → Type w} [Monadm]
(f : α → mPUnit) (as : Arrayα) (start : Nat := as.size)
(stop : Nat := 0) : mPUnit
Array.forRevM.{u, v, w} {α : Type u}
{m : Type v → Type w} [Monadm]
(f : α → mPUnit) (as : Arrayα)
(start : Nat := as.size)
(stop : Nat := 0) : mPUnit
Applies the monadic action f to each element of an array from right to left, in reverse order.
The optional parameters start and stop control the region of the array to which f should be
applied. Iteration proceeds from start (exclusive) to stop (inclusive), so no f is not invoked
unless start>stop. By default, the entire array is used.
Applies a function to each element of an array, returning the array of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new array if the result of each function call is
pointer-equal to its argument.
Array.mapM'.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3}
{β : Type u_1} [Monadm] (f : α → mβ) (as : Arrayα) :
m{ bs // bs.size = as.size }
Array.mapM'.{u_1, u_2, u_3}
{m : Type u_1 → Type u_2} {α : Type u_3}
{β : Type u_1} [Monadm] (f : α → mβ)
(as : Arrayα) :
m{ bs // bs.size = as.size }
Applies the monadic action f to every element in the array, left-to-right, and returns the array
of results. Furthermore, the resulting array's type guarantees that it contains the same number of
elements as the input array.
Array.mapMonoM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1}
[Monadm] (as : Arrayα) (f : α → mα) : m (Arrayα)
Array.mapMonoM.{u_1, u_2}
{m : Type u_1 → Type u_2} {α : Type u_1}
[Monadm] (as : Arrayα) (f : α → mα) :
m (Arrayα)
Applies a monadic function to each element of an array, returning the array of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new array if the result of each function call is
pointer-equal to its argument.
Array.mapFinIdx.{u, v} {α : Type u} {β : Type v} (as : Arrayα)
(f : (i : Nat) → α → i < as.size → β) : Arrayβ
Array.mapFinIdx.{u, v} {α : Type u}
{β : Type v} (as : Arrayα)
(f : (i : Nat) → α → i < as.size → β) :
Arrayβ
Applies a function to each element of the array along with the index at which that element is found,
returning the array of results. In addition to the index, the function is also provided with a proof
that the index is valid.
Array.mapIdx is a variant that does not provide the function with evidence that the index is
valid.
Array.mapFinIdxM.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (as : Arrayα)
(f : (i : Nat) → α → i < as.size → mβ) : m (Arrayβ)
Array.mapFinIdxM.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (as : Arrayα)
(f :
(i : Nat) → α → i < as.size → mβ) :
m (Arrayβ)
Applies the monadic action f to every element in the array, along with the element's index and a
proof that the index is in bounds, from left to right. Returns the array of results.
Array.zip.{u, u_1} {α : Type u} {β : Type u_1} (as : Arrayα)
(bs : Arrayβ) : Array(α × β)
Array.zip.{u, u_1} {α : Type u}
{β : Type u_1} (as : Arrayα)
(bs : Arrayβ) : Array(α × β)
Combines two arrays into an array of pairs in which the first and second components are the
corresponding elements of each input array. The resulting array is the length of the shorter of the
input arrays.
Array.zipWithAll.{u, u_1, u_2} {α : Type u} {β : Type u_1}
{γ : Type u_2} (f : Optionα → Optionβ → γ) (as : Arrayα)
(bs : Arrayβ) : Arrayγ
Array.zipWithAll.{u, u_1, u_2}
{α : Type u} {β : Type u_1}
{γ : Type u_2}
(f : Optionα → Optionβ → γ)
(as : Arrayα) (bs : Arrayβ) : Arrayγ
Applies a function to the corresponding elements of both arrays, stopping when there are no more
elements in either array. If one array is shorter than the other, the function is passed none for
the missing elements.
Returns the array of elements in as for which p returns true.
Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.
Applies the monadic predicate p to every element in the array, in order from left to right, and
returns the array of elements for which p returns true.
Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is checked.
Applies the monadic predicate p on every element in the array in reverse order, from right to
left, and returns those elements for which p returns true. The elements of the returned list are
in the same order as in the input list.
Only elements from start (exclusive) to stop (inclusive) are considered. Elements outside that
range are discarded. Because the array is examined in reverse order, elements are only examined when
start>stop. By default, the entire array is considered.
Array.filterMapM.{u, u_1, u_2} {α : Type u} {m : Type u_1 → Type u_2}
{β : Type u_1} [Monadm] (f : α → m (Optionβ)) (as : Arrayα)
(start : Nat := 0) (stop : Nat := as.size) : m (Arrayβ)
Array.filterMapM.{u, u_1, u_2}
{α : Type u} {m : Type u_1 → Type u_2}
{β : Type u_1} [Monadm]
(f : α → m (Optionβ)) (as : Arrayα)
(start : Nat := 0)
(stop : Nat := as.size) : m (Arrayβ)
Applies a monadic function that returns an Option to each element of an array, collecting the
non-none values.
Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.
Filters an array of syntax, treating every other element as a separator rather than an element to
test with the predicate p. The resulting array contains the tested elements for which p returns
true, separated by the corresponding separator elements.
Filters an array of syntax, treating every other element as a separator rather than an element to
test with the monadic predicate p. The resulting array contains the tested elements for which p
returns true, separated by the corresponding separator elements.
Returns a pair of arrays that together contain all the elements of as. The first array contains
those elements for which p returns true, and the second contains those for which p returns
false.
as.partitionp is equivalent to (as.filterp,as.filter(not∘p)), but it is
more efficient since it only has to do one pass over the array.
Groups the elements of an array xs according to the function key, returning a hash map in which
each group is associated with its key. Groups preserve the relative order of elements in xs.
Array.findIdxM?.{u, u_1} {α : Type u} {m : Type → Type u_1} [Monadm]
(p : α → mBool) (as : Arrayα) : m (OptionNat)
Array.findIdxM?.{u, u_1} {α : Type u}
{m : Type → Type u_1} [Monadm]
(p : α → mBool) (as : Arrayα) :
m (OptionNat)
Finds the index of the first element of an array for which the monadic predicate p returns true.
Elements are examined in order from left to right, and the search is terminated when an element that
satisfies p is found. If no such element exists in the array, then none is returned.
Returns the index of the first element for which p returns true, or none if there is no such
element. The index is returned as a Fin, which guarantees that it is in bounds.
Array.findM?.{u_1} {m : Type → Type u_1} {α : Type} [Monadm]
(p : α → mBool) (as : Arrayα) : m (Optionα)
Array.findM?.{u_1} {m : Type → Type u_1}
{α : Type} [Monadm] (p : α → mBool)
(as : Arrayα) : m (Optionα)
Returns the first element of the array for which the monadic predicate p returns true, or none
if no such element is found. Elements of the array are checked in order.
The monad m is restricted to Type→Type to avoid needing to use ULiftBool in p's type.
Example:
some 1Almost! 6
Almost! 5
#eval#[7,6,5,8,1,2,6].findM?funi=>doifi<5thenreturntrueifi≤6thenIO.printlns!"Almost! {i}"returnfalseAlmost!6Almost!5some1
Array.findRevM?.{w} {α : Type} {m : Type → Type w} [Monadm]
(p : α → mBool) (as : Arrayα) : m (Optionα)
Array.findRevM?.{w} {α : Type}
{m : Type → Type w} [Monadm]
(p : α → mBool) (as : Arrayα) :
m (Optionα)
Returns the last element of the array for which the monadic predicate p returns true, or none
if no such element is found. Elements of the array are checked in reverse, from right to left..
The monad m is restricted to Type→Type to avoid needing to use ULiftBool in p's type.
Array.findSomeM?.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (f : α → m (Optionβ))
(as : Arrayα) : m (Optionβ)
Array.findSomeM?.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : α → m (Optionβ))
(as : Arrayα) : m (Optionβ)
Returns the first non-none result of applying the monadic function f to each element of the
array, in order. Returns none if f returns none for all elements.
Example:
some 10Almost! 6
Almost! 5
#eval#[7,6,5,8,1,2,6].findSomeM?funi=>doifi<5thenreturnsome(i*10)ifi≤6thenIO.printlns!"Almost! {i}"returnnoneAlmost!6Almost!5some10
Array.findSomeRev?.{u, v} {α : Type u} {β : Type v} (f : α → Optionβ)
(as : Arrayα) : Optionβ
Array.findSomeRev?.{u, v} {α : Type u}
{β : Type v} (f : α → Optionβ)
(as : Arrayα) : Optionβ
Returns the first non-none result of applying f to each element of the array in reverse order,
from right to left. Returns none if f returns none for all elements of the array.
Array.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (f : α → m (Optionβ))
(as : Arrayα) : m (Optionβ)
Array.findSomeRevM?.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : α → m (Optionβ))
(as : Arrayα) : m (Optionβ)
Returns the first non-none result of applying the monadic function f to each element of the
array in reverse order, from right to left. Once a non-none result is found, no further elements
are checked. Returns none if f returns none for all elements of the array.
The optional parameters start and stop control the region of the array to be checked. Only the
elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the
entire array is checked.
Returns true if the monadic predicate p returns true for every element of as.
Short-circuits upon encountering the first false. The elements in as are examined in order from
left to right.
The optional parameters start and stop control the region of the array to be checked. Only the
elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the
entire array is checked.
The optional parameters start and stop control the region of the array to be checked. Only the
elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the
entire array is checked.
Returns true if the monadic predicate p returns true for any element of as.
Short-circuits upon encountering the first true. The elements in as are examined in order from
left to right.
The optional parameters start and stop control the region of the array to be checked. Only the
elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the
entire array is checked.
“Attaches” the proof that the elements of xs are in fact elements of xs, producing a new array with
the same elements but in the subtype {x//x∈xs}.
O(1).
This function is primarily used to allow definitions by well-founded
recursion that use higher-order functions (such as
Array.map) to prove that an value taken from a list is smaller than the list. This allows the
well-founded recursion mechanism to prove that the function terminates.
Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such
as map_subtype, and is ideally subsequently simplified away by unattach_attach.
This function is usually inserted automatically by Lean as an intermediate step while proving
termination. It is rarely used explicitly in code. It is introduced as an intermediate step during
the elaboration of definitions by well-founded
recursion. If this function is encountered in a proof
state, the right approach is usually the tactic simp[Array.unattach,-Array.map_subtype].
Array.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {P : α → Prop}
(f : (a : α) → Pa → β) (xs : Arrayα) (H : ∀ (a : α), a ∈ xs → Pa) :
Arrayβ
Array.pmap.{u_1, u_2} {α : Type u_1}
{β : Type u_2} {P : α → Prop}
(f : (a : α) → Pa → β) (xs : Arrayα)
(H : ∀ (a : α), a ∈ xs → Pa) : Arrayβ
Maps a partially defined function (defined on those terms of α that satisfy a predicate P) over
an array xs:Arrayα, given a proof that every element of xs in fact satisfies P.
Array.pmap, named for “partial map,” is the equivalent of Array.map for such partial functions.
A subarray contains an array together with the start and end indices of a region of interest.
Subarrays can be used to avoid copying or allocating space, while being more convenient than
tracking the bounds by hand. The region of interest consists of every index that is both greater
than or equal to start and strictly less than stop.
Extracts an element from the subarray, or returns a default value when the index is out of bounds.
The index is relative to the start and end of the subarray, rather than the underlying array. The
default value is that provided by the Inhabitedα instance.
Subarray.foldlM.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (f : β → α → mβ) (init : β)
(as : Subarrayα) : mβ
Subarray.foldlM.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : β → α → mβ) (init : β)
(as : Subarrayα) : mβ
Folds a monadic operation from left to right over the elements in a subarray.
An accumulator of type β is constructed by starting with init and monadically combining each
element of the subarray with the current accumulator value in turn. The monad in question may permit
early termination or repetition.
Examples:
some "(3)red (5)green (4)blue "#eval#["red","green","blue"].toSubarray.foldlM(init:="")funaccx=>doletl←Option.guard(·≠0)x.lengthreturns!"{acc}({l}){x} "some"(3)red (5)green (4)blue "
#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
let l ← Option.guard (· ≠ 5) x.length
return s!"{acc}({l}){x} "
Folds an operation from right to left over the elements in a subarray.
An accumulator of type β is constructed by starting with init and combining each element of the
subarray with the current accumulator value in turn, moving from the end to the start.
Subarray.foldrM.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (f : α → β → mβ) (init : β)
(as : Subarrayα) : mβ
Subarray.foldrM.{u, v, w} {α : Type u}
{β : Type v} {m : Type v → Type w}
[Monadm] (f : α → β → mβ) (init : β)
(as : Subarrayα) : mβ
Folds a monadic operation from right to left over the elements in a subarray.
An accumulator of type β is constructed by starting with init and monadically combining each
element of the subarray with the current accumulator value in turn, moving from the end to the
start. The monad in question may permit early termination or repetition.
Examples:
some "(4)blue (5)green (3)red "#eval#["red","green","blue"].toSubarray.foldrM(init:="")funxacc=>doletl←Option.guard(·≠0)x.lengthreturns!"{acc}({l}){x} "some"(4)blue (5)green (3)red "
#eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
let l ← Option.guard (· ≠ 5) x.length
return s!"{acc}({l}){x} "
Tests each element in a subarray with a Boolean predicate in reverse order, stopping at the first
element that satisfies the predicate. The element that satisfies the predicate is returned, or
none if no element satisfies the predicate.
Subarray.findRevM?.{w} {α : Type} {m : Type → Type w} [Monadm]
(as : Subarrayα) (p : α → mBool) : m (Optionα)
Subarray.findRevM?.{w} {α : Type}
{m : Type → Type w} [Monadm]
(as : Subarrayα) (p : α → mBool) :
m (Optionα)
Applies a monadic Boolean predicate to each element in a subarray in reverse order, stopping at the
first element that satisfies the predicate. The element that satisfies the predicate is returned, or
none if no element satisfies it.
Subarray.findSomeRevM?.{u, v, w} {α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm] (as : Subarrayα)
(f : α → m (Optionβ)) : m (Optionβ)
Subarray.findSomeRevM?.{u, v, w}
{α : Type u} {β : Type v}
{m : Type v → Type w} [Monadm]
(as : Subarrayα)
(f : α → m (Optionβ)) : m (Optionβ)
Applies a monadic function to each element in a subarray in reverse order, stopping at the first
element for which the function succeeds by returning a value other than none. The succeeding value
is returned, or none if there is no success.
Checks whether all of the elements in a subarray satisfy a Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
Subarray.allM.{u, w} {α : Type u} {m : Type → Type w} [Monadm]
(p : α → mBool) (as : Subarrayα) : mBool
Subarray.allM.{u, w} {α : Type u}
{m : Type → Type w} [Monadm]
(p : α → mBool) (as : Subarrayα) :
mBool
Checks whether all of the elements in a subarray satisfy a monadic Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
