instMonadWriterStateTOfMonad

Mathlib.Control.Monad.Writer

URI: https://scilib.ai/kg/mathlib#instMonadWriterStateTOfMonad

Lean4

instance [Monad M] [MonadWriter ω M] : MonadWriter ω (StateT σ M)
    where
  tell w := (tell w : M _)
  listen x s := (fun ((a, w), s) ↦ ((a, s), w)) <$> listen (x s)
  pass x s := pass <| (fun ((a, f), s) ↦ ((a, s), f)) <$> (x s)

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

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

Разделы

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

Аффилиация

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