English
Find the index of the first element of s that satisfies p: findIndex(p)(s) = (fun o => Option.getD o 0) <$> head (findIndexes p s).
Русский
Найти индекс первого элемента последовательности s, удовлетворяющего p: findIndex(p)(s) = (fun o => Option.getD o 0) <$> head (findIndexes p s).
LaTeX
$$$$ \\mathrm{findIndex}(p)(s) = (\\mathrm{fun\\ o \\Rightarrow \\mathrm{Option.getD}}\\ o\\ 0) \\\\text{ <$> head }(\\mathrm{findIndexes}(p)(s)) $$$$
Lean4
/-- Get the index of the first element of `s` satisfying `p` -/
def findIndex (p : α → Prop) [DecidablePred p] (s : WSeq α) : Computation ℕ :=
(fun o => Option.getD o 0) <$> head (findIndexes p s)
