def Data.List'.nubBy {α : Type u_1} (eq : α → α → Bool) (l : List α) : List α

Remove duplicate elements, preserving first occurrence, using a custom equality. $$\text{nubBy}(eq, [x_1, \ldots, x_n])$$ keeps $x_i$ if no earlier $x_j$ satisfies $\text{eq}(x_j, x_i)$.

Equations

• Data.List'.nubBy eq l = Data.List'.nubBy.go eq l []

def Data.List'.nubBy.go {α : Type u_1} (eq : α → α → Bool) : List α → List α → List α

Equations

• Data.List'.nubBy.go eq [] a✝ = a✝.reverse
• Data.List'.nubBy.go eq (x_2 :: xs) a✝ = if a✝.any (eq x_2) = true then Data.List'.nubBy.go eq xs a✝ else Data.List'.nubBy.go eq xs (x_2 :: a✝)

def Data.List'.nub {α : Type u_1} [BEq α] (l : List α) : List α

Remove duplicate elements using BEq, preserving first occurrence. $$\text{nub} = \text{nubBy}(\text{BEq.beq})$$

Equations

• Data.List'.nub l = Data.List'.nubBy (fun (x1 x2 : α) => x1 == x2) l

@[irreducible]

def Data.List'.groupBy {α : Type u_1} (eq : α → α → Bool) : List α → List (List α)

Group consecutive equal elements by a custom equality. $$\text{groupBy}(eq, [a, a, b, b, b, a]) = [[a, a], [b, b, b], [a]]$$

Equations

• Data.List'.groupBy eq [] = []
• Data.List'.groupBy eq (x_1 :: xs) = (x_1 :: List.takeWhile (eq x_1) xs) :: Data.List'.groupBy eq (List.drop (List.takeWhile (eq x_1) xs).length xs)

def Data.List'.group {α : Type u_1} [BEq α] (l : List α) : List (List α)

Group consecutive equal elements using BEq. $$\text{group} = \text{groupBy}(\text{BEq.beq})$$

Equations

• Data.List'.group l = Data.List'.groupBy (fun (x1 x2 : α) => x1 == x2) l

def Data.List'.transpose {α : Type u_1} (xss : List (List α)) : List (List α)

Transpose a list of lists (rows to columns). $$\text{transpose}([[1,2,3],[4,5,6]]) = [[1,4],[2,5],[3,6]]$$ Uses fuel-based termination.

Equations

• Data.List'.transpose xss = Data.List'.transpose.go xss (List.foldl (fun (acc : Nat) (l : List α) => max acc l.length) 0 xss)

def Data.List'.transpose.go {α : Type u_1} : List (List α) → Nat → List (List α)

Equations

• One or more equations did not get rendered due to their size.
• Data.List'.transpose.go a✝ 0 = []
• Data.List'.transpose.go [] a✝ = []

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

All suffixes, from longest to shortest, including []. Returns NonEmpty since every list has at least the empty suffix. $$\text{tails}([1,2,3]) = [[1,2,3],[2,3],[3],[]]$$

Equations

• Data.List'.tails [] = Data.List.NonEmpty.singleton []
• Data.List'.tails (x_1 :: xs) = { head := x_1 :: xs, tail := (Data.List'.tails xs).toList }

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

All prefixes, from shortest to longest. Returns NonEmpty since every list has at least the empty prefix. $$\text{inits}([1,2,3]) = [[],[1],[1,2],[1,2,3]]$$

Equations

• Data.List'.inits [] = Data.List.NonEmpty.singleton []
• Data.List'.inits (x_1 :: xs) = { head := [], tail := List.map (fun (x : List α) => x_1 :: x) (Data.List'.inits xs).toList }

def Data.List'.subsequences {α : Type u_1} : List α → List (List α)

All subsequences (power set), including []. $$|\text{subsequences}(l)| = 2^{|l|}$$

Equations

• Data.List'.subsequences [] = [[]]
• Data.List'.subsequences (x_1 :: xs) = Data.List'.subsequences xs ++ List.map (fun (x : List α) => x_1 :: x) (Data.List'.subsequences xs)

def Data.List'.permutations {α : Type u_1} : List α → List (List α)

All permutations of a list. $$|\text{permutations}(l)| = |l|!$$

Equations

• Data.List'.permutations [] = [[]]
• Data.List'.permutations (x_1 :: xs) = List.flatMap (Data.List'.insertEverywhere✝ x_1) (Data.List'.permutations xs)

def Data.List'.unfoldr {β : Type u_1} {α : Type u_2} (f : β → Option (α × β)) (seed : β) (fuel : Nat := 10000) : List α

Build a list from a seed by repeatedly applying f. $$\text{unfoldr}(f, b_0) = [a_1, a_2, \ldots]$$ where $f(b_i) = \text{some}(a_{i+1}, b_{i+1})$ until $f(b_n) = \text{none}$. Fuel-limited to ensure termination.

Equations

• Data.List'.unfoldr f seed 0 = []
• Data.List'.unfoldr f seed fuel_2.succ = match f seed with | none => [] | some (a, seed') => a :: Data.List'.unfoldr f seed' fuel_2

def Data.List'.scanr {α : Type u_1} {β : Type u_2} (f : α → β → β) (z : β) : List α → List.NonEmpty β

Right-to-left scan, producing all intermediate accumulators. Returns NonEmpty since the result always includes at least the initial accumulator z. $$\text{scanr}(f, z, [x_1, \ldots, x_n]) = [f(x_1, f(x_2, \ldots f(x_n, z))), \ldots, f(x_n, z), z]$$

Equations

• Data.List'.scanr f z [] = Data.List.NonEmpty.singleton z
• Data.List'.scanr f z (x_1 :: xs) = { head := f x_1 (Data.List'.scanr f z xs).head, tail := (Data.List'.scanr f z xs).toList }

def Data.List'.mapAccumL {σ : Type u_1} {α : Type u_2} {β : Type u_3} (f : σ → α → σ × β) (init : σ) : List α → σ × List β

Left-to-right map with accumulator. $$\text{mapAccumL}(f, s_0, [x_1, \ldots, x_n]) = (s_n, [y_1, \ldots, y_n])$$ where $(s_i, y_i) = f(s_{i-1}, x_i)$.

Equations

• Data.List'.mapAccumL f init [] = (init, [])
• Data.List'.mapAccumL f init (x_1 :: xs) = match f init x_1 with | (s', y) => match Data.List'.mapAccumL f s' xs with | (s'', ys) => (s'', y :: ys)

def Data.List'.mapAccumR {σ : Type u_1} {α : Type u_2} {β : Type u_3} (f : σ → α → σ × β) (init : σ) : List α → σ × List β

Right-to-left map with accumulator. $$\text{mapAccumR}(f, s_0, [x_1, \ldots, x_n]) = (s_n, [y_1, \ldots, y_n])$$ where processing goes right-to-left.

Equations

• Data.List'.mapAccumR f init [] = (init, [])
• Data.List'.mapAccumR f init (x_1 :: xs) = match Data.List'.mapAccumR f init xs with | (s', ys) => match f s' x_1 with | (s'', y) => (s'', y :: ys)

def Data.List'.intercalate {α : Type u_1} (sep : List α) : List (List α) → List α

Intercalate: insert a separator between lists and flatten. $$\text{intercalate}(sep, [l_1, \ldots, l_n]) = l_1 \mathbin{++} sep \mathbin{++} l_2 \mathbin{++} \cdots \mathbin{++} l_n$$

Equations

• Data.List'.intercalate sep [] = []
• Data.List'.intercalate sep [x_1] = x_1
• Data.List'.intercalate sep (x_1 :: xs) = x_1 ++ sep ++ Data.List'.intercalate sep xs

def Data.List'.sortOn {β : Type u_1} {α : Type u_2} [Ord β] (f : α → β) (l : List α) : List α

Sort by a derived key. $$\text{sortOn}(f, l)$$ sorts $l$ by comparing $f(x)$ values.

Equations

• Data.List'.sortOn f l = (l.toArray.qsort fun (a b : α) => compare (f a) (f b) == Ordering.lt).toList

def Data.List'.maximumBy {α : Type u_1} (cmp : α → α → Ordering) : List α → Option α

Maximum element by a custom comparator, or none for empty lists. $$\text{maximumBy}(\text{cmp}, l)$$

Equations

• Data.List'.maximumBy cmp [] = none
• Data.List'.maximumBy cmp (x_1 :: xs) = some (List.foldl (fun (acc y : α) => if (cmp acc y == Ordering.lt) = true then y else acc) x_1 xs)

def Data.List'.minimumBy {α : Type u_1} (cmp : α → α → Ordering) : List α → Option α

Minimum element by a custom comparator, or none for empty lists. $$\text{minimumBy}(\text{cmp}, l)$$

Equations

• Data.List'.minimumBy cmp [] = none
• Data.List'.minimumBy cmp (x_1 :: xs) = some (List.foldl (fun (acc y : α) => if (cmp acc y == Ordering.gt) = true then y else acc) x_1 xs)

def Data.List'.deleteBy {α : Type u_1} (eq : α → α → Bool) (x : α) : List α → List α

Delete the first occurrence matching the predicate. $$\text{deleteBy}(eq, x, l)$$ removes the first $y$ in $l$ with $\text{eq}(x, y)$.

Equations

• Data.List'.deleteBy eq x [] = []
• Data.List'.deleteBy eq x (x_2 :: xs) = if eq x x_2 = true then xs else x_2 :: Data.List'.deleteBy eq x xs

def Data.List'.unionBy {α : Type u_1} (eq : α → α → Bool) (xs ys : List α) : List α

List union by a custom equality. $$\text{unionBy}(eq, l_1, l_2)$$ appends elements of $l_2$ not in $l_1$.

Equations

• Data.List'.unionBy eq xs ys = xs ++ List.filter (fun (y : α) => !xs.any (eq y)) ys

def Data.List'.intersectBy {α : Type u_1} (eq : α → α → Bool) (xs ys : List α) : List α

List intersection by a custom equality. $$\text{intersectBy}(eq, l_1, l_2)$$ keeps elements of $l_1$ that are in $l_2$.

Equations

• Data.List'.intersectBy eq xs ys = List.filter (fun (x : α) => ys.any (eq x)) xs

def Data.List'.insertBy {α : Type u_1} (cmp : α → α → Ordering) (x : α) : List α → List α

Insert into a sorted list, maintaining order. $$\text{insertBy}(\text{cmp}, x, l)$$ places $x$ before the first element greater than it.

Equations

• Data.List'.insertBy cmp x [] = [x]
• Data.List'.insertBy cmp x (x_2 :: xs) = if (cmp x x_2 != Ordering.gt) = true then x :: x_2 :: xs else x_2 :: Data.List'.insertBy cmp x xs

@[inline]

def Data.List'.genericLength {α : Type u_1} (l : List α) : Nat

genericLength is List.length in Lean (which already returns Nat). $$\text{genericLength}(l) = |l|$$

Equations

• Data.List'.genericLength l = l.length

theorem Data.List'.tails_length {α : Type u_1} (l : List α) : (tails l).toList.length = l.length + 1

The tails function produces length + 1 suffixes (as a NonEmpty). $$|\text{tails}(l).\text{toList}| = |l| + 1$$

theorem Data.List'.inits_length {α : Type u_1} (l : List α) : (inits l).toList.length = l.length + 1

The inits function produces length + 1 prefixes (as a NonEmpty). $$|\text{inits}(l).\text{toList}| = |l| + 1$$

theorem Data.List'.tails_nil {α : Type u_1} : tails [] = List.NonEmpty.singleton []

tails of the empty list is the singleton [[]].

theorem Data.List'.inits_nil {α : Type u_1} : inits [] = List.NonEmpty.singleton []

inits of the empty list is the singleton [[]].