English
An auxiliary function extractp(p) on a list returns a pair (optional element satisfying p, the list with that element removed or the original list if none found).
Русский
Вспомогательная функция extractp(p) над списком возвращает пару (опциональный элемент, удовлетворяющий p, список без этого элемента или исходный список, если такой элемент не найден).
LaTeX
$$$\\mathrm{extractp}(p) : \\mathrm{List}\\,\\alpha \\to \\mathrm{Prod}(\\mathrm{Option}\\,\\alpha, \\mathrm{List}\\,\\alpha)$$$
Lean4
/-- `extractp p l` returns a pair of an element `a` of `l` satisfying the predicate
`p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`. -/
def extractp (p : α → Prop) [DecidablePred p] : List α → Option α × List α
| [] => (none, [])
| a :: l =>
if p a then (some a, l)
else
let (a', l') := extractp p l
(a', a :: l')
