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]]

Equations

• List.splitOnPPrepend p [] x✝ = [x✝.reverse]
• List.splitOnPPrepend p (a :: t) x✝ = if p a = true then x✝.reverse :: List.splitOnPPrepend p t [] else List.splitOnPPrepend p t (a :: x✝)

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]]

Equations

• List.splitOnP p l = List.splitOnPPrepend p l []

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

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

Equations

• List.splitOnP.go p l acc = List.splitOnPPrepend p l acc

@[inline]

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

Tail recursive version of splitOnP.

Equations

• List.splitOnPTR p l = List.splitOnPTR.go✝ p l #[] #[]

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

Equations

• List.splitOn a as = List.splitOnP (fun (x : α) => x == a) as