From af5efe0b2d0837b9846a32b32c382d8135ddcd76 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Dec 2022 10:11:42 +0100 Subject: [PATCH] doc: `MonadReader` --- src/Init/Prelude.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index e6a60a86be..95de6a774e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2967,9 +2967,10 @@ end end ReaderT /-- -An implementation of [`MonadReader`]. It does not contain `local` because this -function cannot be lifted using `monadLift`. Instead, the `MonadReaderAdapter` -class provides the more general `adaptReader` function. +An implementation of Haskell's [`MonadReader`] (sans functional dependency; see also `MonadReader` +in this module). It does not contain `local` because this +function cannot be lifted using `monadLift`. `local` is instead provided by +the `MonadWithReader` class as `withReader`. Note: This class can be seen as a simplification of the more "principled" definition ```