comp_traverse

Mathlib.Control.Traversable.Instances

URI: https://scilib.ai/kg/mathlib#Option.comp_traverse

Lean4

theorem comp_traverse {α β γ} (f : β → F γ) (g : α → G β) (x : Option α) :
    Option.traverse (Comp.mk ∘ (f <$> ·) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x) := by
  cases x <;> (simp [Option.traverse, Option.mapM, functor_norm] <;> rfl)

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

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

Разделы

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

Аффилиация

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