This module contains utility functions involving Arrays that are useful in a few places
of the lean code base, but too specialized to live in Init.Data.Array, which arguably
is part of the public, user-facing standard library.
def
Array.filterPairsM
{m : Type → Type u_1}
[Monad m]
{α : Type}
(a : Array α)
(f : α → α → m (Bool × Bool))
:
m (Array α)
Given an array a, runs f xᵢ xⱼ for all i < j, removes those entries for which f returns
false (and will subsequently skip pairs if one element is removed), and returns the array of
remaining elements.
This can be used to remove elements from an array where a “better” element, in some partial order, exists in the array.
Equations
- One or more equations did not get rendered due to their size.