traverse

Mathlib.Algebra.Free

URI: https://scilib.ai/kg/mathlib#FreeAddMagma.traverse

Lean4

/-- `FreeAddMagma` is traversable. -/
protected def traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : α → m β) :
    FreeAddMagma α → m (FreeAddMagma β)
  | FreeAddMagma.of x => FreeAddMagma.of <$> F x
  | x + y => (· + ·) <$> x.traverse F <*> y.traverse F

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

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

Разделы

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

Аффилиация

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