noncomputable def List.splitOnPPrepend {α : Type u_1} (p : α → Bool) (l acc : List α) : List (List α)

Split a list at every element satisfying a predicate, and then prepend acc.reverse to the first element of the result.

• [1, 1, 2, 3, 2, 4, 4].splitOnPPrepend (· == 2) [0, 5] = [[5, 0, 1, 1], [3], [4, 4]]

noncomputable 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.

Examples:

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

@[deprecated List.splitOnPPrepend (since := "2026-02-26")]

noncomputable def List.splitOnP.go {α : Type u_1} (p : α → Bool) (l acc : List α) : List (List α)

@[inline]

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

Tail recursive version of splitOnP.

@[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.

Examples:

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