foldInfoM

Mathlib.Tactic.Linter.HaveLetLinter

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.haveLet.InfoTree.foldInfoM

Lean4

/-- a monadic version of `Lean.Elab.InfoTree.foldInfo`.
Used to infer types inside a `CommandElabM`. -/
def foldInfoM {α m} [Monad m] (f : ContextInfo → Info → α → m α) (init : α) : InfoTree → m α :=
  InfoTree.foldInfo
    (fun ctx i ma => do
      f ctx i (← ma))
    (pure init)

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

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

Разделы

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

Аффилиация

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