English
splitAtPred(p, L) returns the triple (L1, o, L2) where L = L1 ++ a :: L2 with p a = true and L1 contains no earlier element satisfying p; otherwise returns (L, none, []) if no element satisfies p.
Русский
splitAtPred(p,L) возвращает тройку (L1, o, L2), где L = L1 ++ a :: L2 и p a = true, если такой элемент существует, иначе (L, none, []).
LaTeX
$$$\\mathrm{splitAtPred}\\,p:\\; \\text{List }\\alpha \\to \\text{List }\\alpha \\times \\mathrm{Option}\\,\\alpha \\times \\text{List }\\alpha$$$
Lean4
/-- This could be a general list definition, but it is also somewhat specialized to this
application. `splitAtPred p L` will search `L` for the first element satisfying `p`.
If it is found, say `L = l₁ ++ a :: l₂` where `a` satisfies `p` but `l₁` does not, then it returns
`(l₁, some a, l₂)`. Otherwise, if there is no such element, it returns `(L, none, [])`. -/
def splitAtPred {α} (p : α → Bool) : List α → List α × Option α × List α
| [] => ([], none, [])
| a :: as =>
cond (p a) ([], some a, as) <|
let ⟨l₁, o, l₂⟩ := splitAtPred p as
⟨a :: l₁, o, l₂⟩
