New definitions

def List.bagInter {α : Type u_1} [BEq α] : List α → List α → List α

Computes the "bag intersection" of l₁ and l₂, that is, the collection of elements of l₁ which are also in l₂. As each element is identified, it is removed from l₂, so elements are counted with multiplicity.

def List.diff {α : Type u_1} [BEq α] : List α → List α → List α

Computes the difference of l₁ and l₂, by removing each element in l₂ from l₁.

@[inline]

def List.next? {α : Type u_1} : List α → Option (α × List α)

Get the head and tail of a list, if it is nonempty.

@[specialize #[]]

def List.after {α : Type u_1} (p : α → Bool) : List α → List α

after p xs is the suffix of xs after the first element that satisfies p, not including that element.

after      (· == 1) [0, 1, 2, 3] = [2, 3]
drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]

def List.replaceF {α : Type u_1} (f : α → Option α) : List α → List α

Replaces the first element of the list for which f returns some with the returned value.

@[inline]

def List.replaceFTR {α : Type u_1} (f : α → Option α) (l : List α) : List α

Tail-recursive version of replaceF.

@[specialize #[]]

def List.replaceFTR.go {α : Type u_1} (f : α → Option α) : List α → Array α → List α

Auxiliary for replaceFTR: replaceFTR.go f xs acc = acc.toList ++ replaceF f xs.

@[csimp]

theorem List.replaceF_eq_replaceFTR : @replaceF = @replaceFTR

@[inline]

def List.union {α : Type u_1} [BEq α] (l₁ l₂ : List α) : List α

Constructs the union of two lists, by inserting the elements of l₁ in reverse order to l₂. As a result, l₂ will always be a suffix, but only the last occurrence of each element in l₁ will be retained (but order will otherwise be preserved).

@[implicit_reducible]

instance List.instUnionOfBEq_batteries {α : Type u_1} [BEq α] : Union (List α)

@[inline]

def List.inter {α : Type u_1} [BEq α] (l₁ l₂ : List α) : List α

Constructs the intersection of two lists, by filtering the elements of l₁ that are in l₂. Unlike bagInter this does not preserve multiplicity: [1, 1].inter [1] is [1, 1].

@[implicit_reducible]

instance List.instInterOfBEq_batteries {α : Type u_1} [BEq α] : Inter (List α)

def List.splitAtD {α : Type u_1} (n : Nat) (l : List α) (dflt : α) : List α × List α

Split a list at an index. Ensures the left list always has the specified length by right padding with the provided default element.

splitAtD 2 [a, b, c] x = ([a, b], [c])
splitAtD 4 [a, b, c] x = ([a, b, c, x], [])

def List.splitAtD.go {α : Type u_1} (dflt : α) : Nat → List α → List α → List α × List α

Auxiliary for splitAtD: splitAtD.go dflt n l acc = (acc.reverse ++ left, right) if splitAtD n l dflt = (left, right).

def List.splitOnP {α : Type u_1} (P : α → Bool) (l : List α) : List (List α)

Split a list at every element satisfying a predicate. The separators are not in the result.

[1, 1, 2, 3, 2, 4, 4].splitOnP (· == 2) = [[1, 1], [3], [4, 4]]

def List.splitOnP.go {α : Type u_1} (P : α → Bool) : List α → List α → List (List α)

Auxiliary for splitOnP: splitOnP.go xs acc = res' where res' is obtained from splitOnP P xs by prepending acc.reverse to the first element.

@[inline]

def List.splitOnPTR {α : Type u_1} (P : α → Bool) (l : List α) : List (List α)

Tail recursive version of splitOnP.

@[specialize #[]]

def List.splitOnPTR.go {α : Type u_1} (P : α → Bool) : List α → Array α → Array (List α) → List (List α)

Auxiliary for splitOnP: splitOnP.go xs acc r = r.toList ++ res' where res' is obtained from splitOnP P xs by prepending acc.toList to the first element.

@[csimp]

theorem List.splitOnP_eq_splitOnPTR : @splitOnP = @splitOnPTR

@[inline]

def List.splitOn {α : Type u_1} [BEq α] (a : α) (as : List α) : List (List α)

Split a list at every occurrence of a separator element. The separators are not in the result.

[1, 1, 2, 3, 2, 4, 4].splitOn 2 = [[1, 1], [3], [4, 4]]

@[inline]

def List.modifyLast {α : Type u_1} (f : α → α) (l : List α) : List α

Apply f to the last element of l, if it exists.

@[specialize #[]]

def List.modifyLast.go {α : Type u_1} (f : α → α) : List α → Array α → List α

Auxiliary for modifyLast: modifyLast.go f l acc = acc.toList ++ modifyLast f l.

theorem List.headD_eq_head? {α : Type u_1} (l : List α) (a : α) : l.headD a = l.head?.getD a

def List.takeD {α : Type u_1} : Nat → List α → α → List α

Take n elements from a list l. If l has less than n elements, append n - length l elements x.

@[simp]

theorem List.takeD_zero {α : Type u_1} (l : List α) (a : α) : takeD 0 l a = []

@[simp]

theorem List.takeD_succ {α : Type u_1} {n : Nat} (l : List α) (a : α) : takeD (n + 1) l a = l.head?.getD a :: takeD n l.tail a

@[simp]

theorem List.takeD_nil {α : Type u_1} (n : Nat) (a : α) : takeD n [] a = replicate n a

def List.takeDTR {α : Type u_1} (n : Nat) (l : List α) (dflt : α) : List α

Tail-recursive version of takeD.

def List.takeDTR.go {α : Type u_1} (dflt : α) : Nat → List α → Array α → List α

Auxiliary for takeDTR: takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt.

theorem List.takeDTR_go_eq {α✝ : Type u_1} {dflt : α✝} {acc : Array α✝} (n : Nat) (l : List α✝) : takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt

@[csimp]

theorem List.takeD_eq_takeDTR : @takeD = @takeDTR

@[inline]

def List.scanAuxM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β)

Tail-recursive helper function for scanlM and scanrM

@[specialize #[]]

def List.scanAuxM.go {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) : List α → β → List β → m (List β)

Auxiliary for scanAuxM

@[specialize #[]]

def List.foldlIdx {α : Sort u_1} {β : Type u_2} (f : Nat → α → β → α) (init : α) : List β → (start : optParam Nat 0) → α

Fold a list from left to right as with foldl, but the combining function also receives each element's index added to an optional parameter start (i.e. the numbers that f takes as its first argument will be greater than or equal to start and less than start + l.length).

def List.foldrIdx {α : Type u} {β : Type v} (f : Nat → α → β → β) (init : β) (l : List α) (start : Nat := 0) : β

Fold a list from right to left as with foldr, but the combining function also receives each element's index added to an optional parameter start (i.e. the numbers that f takes as its first argument will be greater than or equal to start and less than start + l.length).

@[inline]

def List.foldrIdxTR {α : Type u_1} {β : Type u_2} (f : Nat → α → β → β) (init : β) (l : List α) (start : Nat := 0) : β

A tail-recursive version of foldrIdx.

@[csimp]

theorem List.foldrIdx_eq_foldrIdxTR : @foldrIdx = @foldrIdxTR

@[inline]

def List.findIdxs {α : Type u_1} (p : α → Bool) (l : List α) (start : Nat := 0) : List Nat

findIdxs p l s is the list of indexes of elements of l that satisfy p, added to an optional parameter s (so that the members of findIdxs p l s will be greater than or equal to s and less than l.length + s).

@[inline]

def List.findIdxsValues {α : Type u_1} (p : α → Bool) (l : List α) (start : Nat := 0) : List (Nat × α)

Returns the elements of l that satisfy p together with their indexes in l added to an optional parameter start. The returned list is ordered by index. We have l.findIdxsValues p s = (l.findIdxs p s).zip (l.filter p).

@[deprecated List.findIdxsValues (since := "2025-11-06")]

def List.indexsValues {α : Type u_1} (p : α → Bool) (l : List α) (start : Nat := 0) : List (Nat × α)

Alias of List.findIdxsValues.

---

Returns the elements of l that satisfy p together with their indexes in l added to an optional parameter start. The returned list is ordered by index. We have l.findIdxsValues p s = (l.findIdxs p s).zip (l.filter p).

@[inline]

def List.findIdxNth {α : Type u_1} (p : α → Bool) (xs : List α) (n : Nat) : Nat

findIdxNth p xs n returns the index of the nth element for which p returns true. For example:

findIdxNth (· < 3) [5, 1, 3, 2, 4, 0, 1, 4] 2 = 5

@[specialize #[]]

def List.findIdxNth.go {α : Type u_1} (p : α → Bool) (xs : List α) (n s : Nat) : Nat

Auxiliary for findIdxNth: findIdxNth.go p l n acc = findIdxNth p l n + acc.

@[inline]

def List.idxsOf {α : Type u_1} [BEq α] (a : α) (xs : List α) (start : Nat := 0) : List Nat

idxsOf a l s is the list of all indexes of a in l, added to an optional parameter s. For example:

idxsOf b [a, b, a, a] = [1]
idxsOf a [a, b, a, a] 5 = [5, 7, 8]

@[deprecated List.idxsOf (since := "2025-11-06")]

def List.indexesOf {α : Type u_1} [BEq α] (a : α) (xs : List α) (start : Nat := 0) : List Nat

Alias of List.idxsOf.

---

idxsOf a l s is the list of all indexes of a in l, added to an optional parameter s. For example:

idxsOf b [a, b, a, a] = [1]
idxsOf a [a, b, a, a] 5 = [5, 7, 8]

def List.idxOfNth {α : Type u_1} [BEq α] (a : α) (xs : List α) (n : Nat) : Nat

idxOfNth a xs n returns the index of the nth instance of a in xs, counting from 0.

For example:

idxOfNth 1 [5, 1, 3, 2, 4, 0, 1, 4] 1 = 6

def List.countPBefore {α : Type u_1} (p : α → Bool) (xs : List α) (i : Nat) : Nat

countPBefore p xs i hip counts the number of x in xs before the ith index for which p x = true.

For example:

countPBefore (· < 3) [5, 1, 3, 2, 4, 0, 1, 4] 5 = 2

@[specialize #[]]

def List.countPBefore.go {α : Type u_1} (p : α → Bool) (xs : List α) (i s : Nat) : Nat

Auxiliary for countPBefore: countPBefore.go p l i acc = countPBefore p l i + acc.

def List.countBefore {α : Type u_1} [BEq α] (a : α) : List α → Nat → Nat

countBefore a xs n counts the number of x in xs before the ith index for which x == a is true.

For example:

countBefore 1 [5, 1, 3, 2, 4, 0, 1, 4] 6 = 1

@[inline]

def List.lookmap {α : Type u_1} (f : α → Option α) (l : List α) : List α

lookmap is a combination of lookup and filterMap. lookmap f l will apply f : α → Option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

@[specialize #[]]

def List.lookmap.go {α : Type u_1} (f : α → Option α) : List α → Array α → List α

Auxiliary for lookmap: lookmap.go f l acc = acc.toList ++ lookmap f l.

def List.inits {α : Type u_1} : List α → List (List α)

inits l is the list of initial segments of l.

inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]

def List.initsTR {α : Type u_1} (l : List α) : List (List α)

Tail-recursive version of inits.

@[csimp]

theorem List.inits_eq_initsTR : @inits = @initsTR

def List.tails {α : Type u_1} : List α → List (List α)

tails l is the list of terminal segments of l.

tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]

def List.tailsTR {α : Type u_1} (l : List α) : List (List α)

Tail-recursive version of tails.

def List.tailsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) : List (List α)

Auxiliary for tailsTR: tailsTR.go l acc = acc.toList ++ tails l.

@[csimp]

theorem List.tails_eq_tailsTR : @tails = @tailsTR

def List.sublists' {α : Type u_1} (l : List α) : List (List α)

sublists' l is the list of all (non-contiguous) sublists of l. It differs from sublists only in the order of appearance of the sublists; sublists' uses the first element of the list as the MSB, sublists uses the first element of the list as the LSB.

sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]

def List.sublists {α : Type u_1} (l : List α) : List (List α)

sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]

def List.sublistsFast {α : Type u_1} (l : List α) : List (List α)

A version of List.sublists that has faster runtime performance but worse kernel performance

@[csimp]

theorem List.sublists_eq_sublistsFast : @sublists = @sublistsFast

inductive List.Forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : List α → List β → Prop

Forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

• nil {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : Forall₂ R [] []

  Two nil lists are Forall₂-related

• cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β} : R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)

  Two cons lists are related by Forall₂ R if the heads are related by R and the tails are related by Forall₂ R

@[simp]

theorem List.forall₂_cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β} : Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ Forall₂ R l₁ l₂

def List.all₂ {α : Type u_1} {β : Type u_2} (r : α → β → Bool) : List α → List β → Bool

Check for all elements a, b, where a and b are the nth element of the first and second List respectively, that r a b = true.

@[simp]

theorem List.all₂_eq_true {α : Type u_1} {β : Type u_2} {r : α → β → Bool} (l₁ : List α) (l₂ : List β) : all₂ r l₁ l₂ = true ↔ Forall₂ (fun (x1 : α) (x2 : β) => r x1 x2 = true) l₁ l₂

@[implicit_reducible]

instance List.instDecidableForall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [(a : α) → (b : β) → Decidable (R a b)] (l₁ : List α) (l₂ : List β) : Decidable (Forall₂ R l₁ l₂)

def List.transpose {α : Type u_1} (l : List (List α)) : List (List α)

Transpose of a list of lists, treated as a matrix.

transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]

def List.transpose.pop {α : Type u_1} (old : List α) : List α → Id (List α × List α)

pop : List α → StateM (List α) (List α) transforms the input list old by taking the head of the current state and pushing it on the head of old. If the state list is empty, then old is left unchanged.

def List.transpose.go {α : Type u_1} (l : List α) (acc : Array (List α)) : Array (List α)

go : List α → Array (List α) → Array (List α) handles the insertion of a new list into all the lists in the array: go [a, b, c] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃]. If the new list is too short, the later lists are unchanged, and if it is too long the array is extended:

go [a] #[l₁, l₂, l₃] = #[a::l₁, l₂, l₃]
go [a, b, c, d] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃, [d]]

def List.sections {α : Type u_1} : List (List α) → List (List α)

List of all sections through a list of lists. A section of [L₁, L₂, ..., Lₙ] is a list whose first element comes from L₁, whose second element comes from L₂, and so on.

def List.sectionsTR {α : Type u_1} (L : List (List α)) : List (List α)

Optimized version of sections.

def List.sectionsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) : Array (List α)

go : List α → Array (List α) → Array (List α) inserts one list into the accumulated list of sections acc: go [a, b] #[l₁, l₂] = [a::l₁, b::l₁, a::l₂, b::l₂].

theorem List.sections_eq_nil_of_isEmpty {α : Type u_1} {L : List (List α)} : L.any isEmpty = true → L.sections = []

@[csimp]

theorem List.sections_eq_sectionsTR : @sections = @sectionsTR

def List.extractP {α : Type u_1} (p : α → Bool) (l : List α) : Option α × List α

extractP p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

def List.extractP.go {α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → Option α × List α

Auxiliary for extractP: extractP.go p l xs acc = (some a, acc.toList ++ out) if extractP p xs = (some a, out), and extractP.go p l xs acc = (none, l) if extractP p xs = (none, _).

def List.revzip {α : Type u_1} (l : List α) : List (α × α)

revzip l returns a list of pairs of the elements of l paired with the elements of l in reverse order.

revzip [1, 2, 3, 4, 5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]

def List.product {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : List (α × β)

product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]

def List.productTR {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : List (α × β)

Optimized version of product.

@[csimp]

theorem List.product_eq_productTR : @product = @productTR

def List.sigma {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) : List ((a : α) × σ a)

sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]

def List.sigmaTR {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) : List ((a : α) × σ a)

Optimized version of sigma.

@[csimp]

theorem List.sigma_eq_sigmaTR : @List.sigma = @sigmaTR

def List.ofFnNthVal {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) : Option α

ofFnNthVal f i returns some (f i) if i < n and none otherwise.

def List.Disjoint {α : Type u_1} (l₁ l₂ : List α) : Prop

Disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

def List.takeWhile₂ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) : List α → List β → List α × List β

Returns the longest initial prefix of two lists such that they are pairwise related by R.

takeWhile₂ (· < ·) [1, 2, 4, 5] [5, 4, 3, 6] = ([1, 2], [5, 4])

@[inline]

def List.takeWhile₂TR {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (as : List α) (bs : List β) : List α × List β

Tail-recursive version of takeWhile₂.

@[specialize #[]]

def List.takeWhile₂TR.go {α : Type u_1} {β : Type u_2} (R : α → β → Bool) : List α → List β → List α → List β → List α × List β

Auxiliary for takeWhile₂TR: takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ as', acca.reverse ++ bs') if takeWhile₂ R as bs = (as', bs').

@[csimp]

theorem List.takeWhile₂_eq_takeWhile₂TR : @takeWhile₂ = @takeWhile₂TR

def List.pwFilter {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) : List α

pwFilter R l is a maximal sublist of l which is Pairwise R. pwFilter (·≠·) is the erase duplicates function (cf. eraseDups), and pwFilter (·<·) finds a maximal increasing subsequence in l. For example,

pwFilter (·<·) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]

inductive List.IsChain {α : Type u_1} (R : α → α → Prop) : List α → Prop

IsChain R l means that R holds between adjacent elements of l. Example:

IsChain R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d

• nil {α : Type u_1} {R : α → α → Prop} : IsChain R []

  A list of length 0 is a chain.

• singleton {α : Type u_1} {R : α → α → Prop} (a : α) : IsChain R [a]

  A list of length 1 is a chain.

• cons_cons {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α} (hr : R a b) (h : IsChain R (b :: l)) : IsChain R (a :: b :: l)

  If a relates to b and b::l is a chain, then a :: b :: l is also a chain.

@[simp]

theorem List.isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

@[implicit_reducible]

instance List.instDecidableIsChainOfDecidableRel {α : Type u_1} {R : α → α → Prop} [h : DecidableRel R] (l : List α) : Decidable (IsChain R l)

def List.instDecidableIsChainOfDecidableRel.go {α : Type u_1} {R : α → α → Prop} [h : DecidableRel R] (a : α) (l : List α) : Decidable (IsChain R (a :: l))

@[deprecated List.IsChain (since := "2025-09-19")]

def List.Chain {α : Type u_1} : (α → α → Prop) → α → List α → Prop

Chain R a l means that R holds between adjacent elements of a::l.

Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d

@[deprecated List.IsChain.singleton (since := "2025-09-19")]

theorem List.Chain.nil {α : Type u_1} {R : α → α → Prop} {a : α} : Chain R a []

A list of length 1 is a chain.

@[deprecated List.IsChain.cons_cons (since := "2025-09-19")]

theorem List.Chain.cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {b : α✝} {l : List α✝} {a : α✝} : R a b → Chain R b l → Chain R a (b :: l)

If a relates to b and b::l is a chain, then a :: b :: l is also a chain.

@[deprecated List.IsChain (since := "2025-09-19")]

def List.Chain' {α : Type u_1} : (α → α → Prop) → List α → Prop

Chain' R l means that R holds between adjacent elements of l.

Chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d

@[reducible, inline, deprecated "use `reverse ∘ eraseDups ∘ reverse` or just `eraseDups`" (since := "2026-01-03")]

abbrev List.eraseDup {α : Type u_1} [BEq α] : List α → List α

Deprecated: Use reverse ∘ eraseDups ∘ reverse or just eraseDups instead.

@[inline]

def List.rotate {α : Type u_1} (l : List α) (n : Nat) : List α

rotate l n rotates the elements of l to the left by n

rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]

def List.rotate' {α : Type u_1} : List α → Nat → List α

rotate' is the same as rotate, but slower. Used for proofs about rotate

def List.mapDiagM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → α → m β) (l : List α) : m (List β)

mapDiagM f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

mapDiagM f [1, 2, 3] =
  return [← f 1 1, ← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]

def List.mapDiagM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → α → m β) : List α → Array β → m (List β)

Auxiliary for mapDiagM: mapDiagM.go as f acc = (acc.toList ++ ·) <$> mapDiagM f as

def List.forDiagM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → α → m PUnit) : List α → m PUnit

forDiagM f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

forDiagM f [1, 2, 3] = do f 1 1; f 1 2; f 1 3; f 2 2; f 2 3; f 3 3

def List.getRest {α : Type u_1} [DecidableEq α] : List α → List α → Option (List α)

getRest l l₁ returns some l₂ if l = l₁ ++ l₂. If l₁ is not a prefix of l, returns none

def List.dropSlice {α : Type u_1} : Nat → Nat → List α → List α

List.dropSlice n m xs removes a slice of length m at index n in list xs.

@[inline]

def List.dropSliceTR {α : Type u_1} (n m : Nat) (l : List α) : List α

Optimized version of dropSlice.

def List.dropSliceTR.go {α : Type u_1} (l : List α) (m : Nat) : List α → Nat → Array α → List α

Auxiliary for dropSliceTR: dropSliceTR.go l m xs n acc = acc.toList ++ dropSlice n m xs unless n ≥ length xs, in which case it is l.

theorem List.dropSlice_zero₂ {α : Type u_1} (n : Nat) (l : List α) : dropSlice n 0 l = l

@[csimp]

theorem List.dropSlice_eq_dropSliceTR : @dropSlice = @dropSliceTR

def List.zipWithLeft' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → List γ × List β

Left-biased version of List.zipWith. zipWithLeft' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ. Returns the results of the f applications and the remaining bs.

zipWithLeft' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipWithLeft' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])

@[inline]

def List.zipWithLeft'TR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β) : List γ × List β

Tail-recursive version of zipWithLeft'.

def List.zipWithLeft'TR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → Array γ → List γ × List β

Auxiliary for zipWithLeft'TR: zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l.

@[csimp]

theorem List.zipWithLeft'_eq_zipWithLeft'TR : @zipWithLeft' = @zipWithLeft'TR

@[inline]

def List.zipWithRight' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) : List γ × List α

Right-biased version of List.zipWith. zipWithRight' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ. Returns the results of the f applications and the remaining as.

zipWithRight' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipWithRight' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])

@[inline]

def List.zipLeft' {α : Type u_1} {β : Type u_2} : List α → List β → List (α × Option β) × List β

Left-biased version of List.zip. zipLeft' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none. Also returns the remaining bs.

zipLeft' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipLeft' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
zipLeft' = zipWithLeft' prod.mk

@[inline]

def List.zipRight' {α : Type u_1} {β : Type u_2} : List α → List β → List (Option α × β) × List α

Right-biased version of List.zip. zipRight' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none. Also returns the remaining as.

zipRight' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipRight' [1, 2] ['a'] = ([(some 1, 'a')], [2])
zipRight' = zipWithRight' prod.mk

def List.zipWithLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → List γ

Left-biased version of List.zipWith. zipWithLeft f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs‌∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ.

zipWithLeft prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipWithLeft prod.mk [1] ['a', 'b'] = [(1, some 'a')]
zipWithLeft f as bs = (zipWithLeft' f as bs).fst

@[inline]

def List.zipWithLeftTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β) : List γ

Tail-recursive version of zipWithLeft.

def List.zipWithLeftTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → Array γ → List γ

Auxiliary for zipWithLeftTR: zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l.

@[csimp]

theorem List.zipWithLeft_eq_zipWithLeftTR : @zipWithLeft = @zipWithLeftTR

@[inline]

def List.zipWithRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) : List γ

Right-biased version of List.zipWith. zipWithRight f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs‌∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ.

zipWithRight prod.mk [1, 2] ['a'] = [(some 1, 'a')]
zipWithRight prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipWithRight f as bs = (zipWithRight' f as bs).fst

@[inline]

def List.zipLeft {α : Type u_1} {β : Type u_2} : List α → List β → List (α × Option β)

Left-biased version of List.zip. zipLeft as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none.

zipLeft [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipLeft [1] ['a', 'b'] = [(1, some 'a')]
zipLeft = zipWithLeft prod.mk

@[inline]

def List.zipRight {α : Type u_1} {β : Type u_2} : List α → List β → List (Option α × β)

Right-biased version of List.zip. zipRight as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none.

zipRight [1, 2] ['a'] = [(some 1, 'a')]
zipRight [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipRight = zipWithRight prod.mk

@[inline]

def List.allSome {α : Type u_1} (l : List (Option α)) : Option (List α)

If all elements of xs are some xᵢ, allSome xs returns the xᵢ. Otherwise it returns none.

allSome [some 1, some 2] = some [1, 2]
allSome [some 1, none  ] = none

@[deprecated "Deprecated without replacement." (since := "2025-08-07")]

def List.fillNones {α : Type u_1} : List (Option α) → List α → List α

fillNones xs ys replaces the nones in xs with elements of ys. If there are not enough ys to replace all the nones, the remaining nones are dropped from xs.

fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]

def List.takeList {α : Type u_1} : List α → List Nat → List (List α) × List α

takeList as ns extracts successive sublists from as. For ns = n₁ ... nₘ, it first takes the n₁ initial elements from as, then the next n₂ ones, etc. It returns the sublists of as -- one for each nᵢ -- and the remaining elements of as. If as does not have at least as many elements as the sum of the nᵢ, the corresponding sublists will have less than nᵢ elements.

takeList ['a', 'b', 'c', 'd', 'e'] [2, 1, 1] = ([['a', 'b'], ['c'], ['d']], ['e'])
takeList ['a', 'b'] [3, 1] = ([['a', 'b'], []], [])

@[inline]

def List.takeListTR {α : Type u_1} (xs : List α) (ns : List Nat) : List (List α) × List α

Tail-recursive version of takeList.

def List.takeListTR.go {α : Type u_1} : List Nat → List α → Array (List α) → List (List α) × List α

Auxiliary for takeListTR: takeListTR.go as as' acc = acc.toList ++ takeList as as'.

@[csimp]

theorem List.takeList_eq_takeListTR : @takeList = @takeListTR

def List.toChunksAux {α : Type u_1} (n : Nat) : List α → Nat → List α × List (List α)

Auxliary definition used to define toChunks. toChunksAux n xs i returns (xs.take i, (xs.drop i).toChunks (n+1)), that is, the first i elements of xs, and the remaining elements chunked into sublists of length n+1.

def List.toChunks {α : Type u_1} : Nat → List α → List (List α)

xs.toChunks n splits the list into sublists of size at most n, such that (xs.toChunks n).join = xs.

[1, 2, 3, 4, 5, 6, 7, 8].toChunks 10 = [[1, 2, 3, 4, 5, 6, 7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 3 = [[1, 2, 3], [4, 5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 2 = [[1, 2], [3, 4], [5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 0 = [[1, 2, 3, 4, 5, 6, 7, 8]]

def List.toChunks.go {α : Type u_1} (n : Nat) : List α → Array α → Array (List α) → List (List α)

Auxliary definition used to define toChunks. toChunks.go xs acc₁ acc₂ pushes elements into acc₁ until it reaches size n, then it pushes the resulting list to acc₂ and continues until xs is exhausted.

We add some n-ary versions of List.zipWith for functions with more than two arguments. These can also be written in terms of List.zip or List.zipWith. For example, zipWith₃ f xs ys zs could also be written as zipWith id (zipWith f xs ys) zs or as (zip xs <| zip ys zs).map fun ⟨x, y, z⟩ => f x y z.

def List.zipWith₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → δ) : List α → List β → List γ → List δ

Ternary version of List.zipWith.

def List.zipWith₄ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : α → β → γ → δ → ε) : List α → List β → List γ → List δ → List ε

Quaternary version of List.zipWith.

def List.zipWith₅ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β → γ → δ → ε → ζ) : List α → List β → List γ → List δ → List ε → List ζ

Quinary version of List.zipWith.

def List.mapWithPrefixSuffixAux {α : Type u_1} {β : Type u_2} (f : List α → α → List α → β) : List α → List α → List β

An auxiliary function for List.mapWithPrefixSuffix.

def List.mapWithPrefixSuffix {α : Type u_1} {β : Type u_2} (f : List α → α → List α → β) (l : List α) : List β

List.mapWithPrefixSuffix f l maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f pref a suff. Example: if f : list Nat → Nat → list Nat → β, List.mapWithPrefixSuffix f [1, 2, 3] will produce the list [f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []].

def List.mapWithComplement {α : Type u_1} {β : Type u_2} (f : α → List α → β) : List α → List β

List.mapWithComplement f l is a variant of List.mapWithPrefixSuffix that maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f a (pref ++ suff), i.e., the list input to f is l with a removed. Example: if f : Nat → list Nat → β, List.mapWithComplement f [1, 2, 3] will produce the list [f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]].

def List.traverse {F : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative F] (f : α → F β) : List α → F (List β)

Map each element of a List to an action, evaluate these actions in order, and collect the results.

def List.Subperm {α : Type u_1} (l₁ l₂ : List α) : Prop

Subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the ≤ relation on multisets.

def List.«term_<+~_» : Lean.TrailingParserDescr

Subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the ≤ relation on multisets.

def List.isSubperm {α : Type u_1} [BEq α] (l₁ l₂ : List α) : Bool

O(|l₁| * (|l₁| + |l₂|)). Computes whether l₁ is a sublist of a permutation of l₂. See isSubperm_iff for a characterization in terms of List.Subperm.

def List.insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : List α

O(|l|). Inserts a in l right before the first element such that p is true, or at the end of the list if p always false on l.

def List.insertP.loop {α : Type u_1} (p : α → Bool) (a : α) : List α → List α → List α

Inner loop for insertP. Tail recursive.

def List.dropPrefix? {α : Type u_1} [BEq α] : List α → List α → Option (List α)

dropPrefix? l p returns some r if l = p' ++ r for some p' which is paiwise == to p, and none otherwise.

def List.dropSuffix? {α : Type u_1} [BEq α] (l s : List α) : Option (List α)

dropSuffix? l s returns some r if l = r ++ s' for some s' which is paiwise == to s, and none otherwise.

def List.dropInfix? {α : Type u_1} [BEq α] (l i : List α) : Option (List α × List α)

dropInfix? l i returns some (p, s) if l = p ++ i' ++ s for some i' which is paiwise == to i, and none otherwise.

Note that this is an inefficient implementation, and if computation time is a concern you should be using the Knuth-Morris-Pratt algorithm as implemented in Batteries.Data.List.Matcher.

def List.dropInfix?.go {α : Type u_1} [BEq α] (i : List α) : List α → List α → Option (List α × List α)

Inner loop for dropInfix?.

def List.prod {α : Type u_1} [Mul α] [One α] (xs : List α) : α

Computes the product of the elements of a list.

Examples:

[a, b, c].prod = a * (b * (c * 1)) [2, 3, 5].prod = 30

def List.partialSums {α : Type u_1} [Add α] [Zero α] (l : List α) : List α

Computes the partial sums of the elements of a list.

Examples:

[a, b, c].partialSums = [0, 0 + a, (0 + a) + b, ((0 + a) + b) + c] [1, 2, 3].partialSums = [0, 1, 3, 6]

def List.partialProds {α : Type u_1} [Mul α] [One α] (l : List α) : List α

Computes the partial products of the elements of a list.

Examples:

[a, b, c].partialProds = [1, 1 * a, (1 * a) * b, ((1 * a) * b) * c] [2, 3, 5].partialProds = [1, 2, 6, 30]