List.splitOn

@[simp]

theorem List.splitOn_nil {α : Type u_1} [DecidableEq α] (a : α) : splitOn a [] = [[]]

@[simp]

theorem List.splitOnP_nil {α : Type u_1} (p : α → Bool) : splitOnP p [] = [[]]

theorem List.splitOnP.go_ne_nil {α : Type u_1} (p : α → Bool) (xs acc : List α) : go p xs acc ≠ []

theorem List.splitOnP.go_acc {α : Type u_1} (p : α → Bool) (xs acc : List α) : go p xs acc = modifyHead (fun (x : List α) => acc.reverse ++ x) (splitOnP p xs)

theorem List.splitOnP_ne_nil {α : Type u_1} (p : α → Bool) (xs : List α) : splitOnP p xs ≠ []

@[simp]

theorem List.splitOnP_cons {α : Type u_1} (p : α → Bool) (x : α) (xs : List α) : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

theorem List.splitOnP_spec {α : Type u_1} (p : α → Bool) (as : List α) : (zipWith (fun (x1 x2 : List α) => x1 ++ x2) (splitOnP p as) (map (fun (x : α) => [x]) (filter p as) ++ [[]])).flatten = as

The original list L can be recovered by flattening the lists produced by splitOnP p L, interspersed with the elements L.filter p.

theorem List.splitOnP_spec.flatten_zipWith {α : Type u_1} {xs ys : List (List α)} {a : α} (hxs : xs ≠ []) (hys : ys ≠ []) : (zipWith (fun (x x_1 : List α) => x ++ x_1) (modifyHead (cons a) xs) ys).flatten = a :: (zipWith (fun (x x_1 : List α) => x ++ x_1) xs ys).flatten

theorem List.splitOnP_eq_single {α : Type u_1} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) : splitOnP p xs = [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

theorem List.splitOnP_first {α : Type u_1} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) (sep : α) (hsep : p sep = true) (as : List α) : splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

theorem List.intercalate_splitOn {α : Type u_1} (xs : List α) (x : α) [DecidableEq α] : [x].intercalate (splitOn x xs) = xs

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u_1} (ls : List (List α)) [DecidableEq α] (x : α) (hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l) (hls : ls ≠ []) : splitOn x ([x].intercalate ls) = ls

splitOn x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x