monad

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.monad

Lean4

/-- Unfortunately, `WSeq` is not a lawful monad, because it does not satisfy the monad laws exactly,
only up to sequence equivalence. Furthermore, even quotienting by the equivalence is not sufficient,
because the join operation involves lists of quotient elements, with a lifted equivalence relation,
and pure quotients cannot handle this type of construction. -/
instance monad : Monad WSeq where
  map := @map
  pure := @ret
  bind := @bind

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

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

Разделы

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

Аффилиация

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