Reader and local

Stream: lean4

[David Thrane Christiansen]

The documentation for MonadReaderOf states:

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.

And indeed, there is no local.

However, grepping the Lean 4 source doesn't find any occurrences of adaptReader other than this doc comment.

I have two questions:

1. Where can I learn more about adaptReader? Locally overriding a Reader effect is a highly useful thing to do, after all!
2. If I need to use something like local, is there a better way to do it than by defining my own MTL-style instance pile?

Thanks!

[Jannis Limperg]

I think you're looking for withReader.

[David Thrane Christiansen]

Ah, great, it's a docs bug! I'll open an issue.

[David Thrane Christiansen]

And thanks :-)

[Sebastian Ullrich]

Fixed, thanks!

[Sebastian Ullrich]

Oops, too slow

[David Thrane Christiansen]

All good :-)