max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: MonadReader

Browse source
This commit is contained in:
Sebastian Ullrich 2022-12-01 10:11:42 +01:00
parent 50b2ad89b4
commit af5efe0b2d
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Prelude.lean
View file

@ -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
```