findM?'

Mathlib.Data.List.Defs

URI: https://scilib.ai/kg/mathlib#List.findM?'

Lean4

/-- `findM? p l` returns the first element `a` of `l` for which `p a` returns
true. `findM?` short-circuits, so `p` is not necessarily run on every `a` in
`l`. This is a monadic version of `List.find`. -/
def findM?' {m : Type u → Type v} [Monad m] {α : Type u} (p : α → m (ULift Bool)) : List α → m (Option α)
  | [] => pure none
  | x :: xs => do
    let ⟨px⟩ ← p x
    if px then
      pure (some x)
    else
      findM?' p xs

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru