Skip to content

Commit

Permalink
doc: missing (type := true) in reader monad example (#6196)
Browse files Browse the repository at this point in the history
This PR adds missing `(types := true)` to `#reduce` example in [Readers
example](https://lean-lang.org/lean4/doc/monads/readers.lean.html).
Since [4.10](https://lean-lang.org/blog/2024-8-1-lean-4100/) the `(types
:= true)` is necessary for the `ReaderM Environment String` type to be
reduced into `Environment → String`.
  • Loading branch information
jsr-p authored Dec 7, 2024
1 parent 6447fda commit 762c575
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/monads/readers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ You might be wondering, how does the context actually move through the `ReaderM`
add an input argument to a function by modifying its return type? There is a special command in
Lean that will show you the reduced types:
-/
#reduce ReaderM Environment String -- Environment → String
#reduce (types := true) ReaderM Environment String -- Environment → String
/-!
And you can see here that this type is actually a function! It's a function that takes an
`Environment` as input and returns a `String`.
Expand Down Expand Up @@ -196,4 +196,4 @@ entirely.
Now it's time to move on to [StateM Monad](states.lean.md) which is like a `ReaderM` that is
also updatable.
-/
-/

0 comments on commit 762c575

Please sign in to comment.