firstDeclM

Mathlib.Lean.LocalContext

URI: https://scilib.ai/kg/mathlib#Lean.LocalContext.firstDeclM

Lean4

/-- Return the result of `f` on the first local declaration on which `f` succeeds. -/
@[specialize]
def firstDeclM (lctx : LocalContext) (f : LocalDecl → m β) : m β := do
  match (← lctx.findDeclM? (optional ∘ f)) with
  | none =>
    failure
  | some b =>
    pure b

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

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

Разделы

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

Аффилиация

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