instMonadWriterReaderT

Mathlib.Control.Monad.Writer

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

Lean4

instance [MonadWriter ω M] : MonadWriter ω (ReaderT ρ M)
    where
  tell w := (tell w : M _)
  listen x r := listen <| x r
  pass x r := pass <| x r

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

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

Разделы

Аффилиация

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