Skip to content

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Sep 1, 2025

This PR allows the use of StateT σ m when only Functor m is available.

This also results in a possibly more efficient StateT.map, since it now uses the map from the underlying functor rather than discarding it and rebuilding with bind.

This also results in a possibly more efficient `StateT.map`, since it now uses the `map` from the underlying functor rather than discarding it and rebuilding with `bind`.
@eric-wieser
Copy link
Contributor Author

changelog-library

@github-actions github-actions bot added the changelog-library Library label Sep 2, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 2, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f1737737f0699ac8417605dc0148f079b5c8dd53 --onto c4e5f575121d508e02c82edd603f3c2808bdb5bc. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-02 12:12:33)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f1737737f0699ac8417605dc0148f079b5c8dd53 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-02 12:12:34)

@eric-wieser eric-wieser marked this pull request as ready for review September 2, 2025 14:26
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 10, 2025
@eric-wieser
Copy link
Contributor Author

The failures here look a little annoying; I think that #11470 (and some cleanup on top of it) will help

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants