fix: missing (type := true) in reader monad example

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

fix: missing (type := true) in reader monad example #6196

Open jsr-p opened 1 day ago

jsr-p commented 1 day ago

This PR adds missing (types := true) to #reduce example in Readers example. Since 4.10 the (types := true) is necessary for the ReaderM Environment String type to be reduced into Environment → String.

leanprover-community-bot commented 1 day ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4e885be96d82c522af4acb9ce9afe77e5aea7feb --onto ba3f2b3ecf8967410f3498e2835b883601f03967. (2024-11-24 10:15:10)
✅ Mathlib branch lean-pr-testing-6196 has successfully built against this PR. (2024-11-25 08:09:42) View Log