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 α)

Compares each element of an array with all later elements using f. For each comparison, f determines whether to keep both of its arguments. If f returns false for an argument, that argument is removed from the array and does not participate in subsequent comparisons. Those elements that were not discarded are returned.

This can be used to remove elements from an array where a “better” element, in some partial order, exists in the array.

Example:

#eval #["a", "r", "red", "x", "r"].filterPairsM fun x y =>
  pure (!(x.isPrefixOf y), true)

#["a", "red", "x", "r"]

Equations

• One or more equations did not get rendered due to their size.