Skip to content

fix: remove accidental type monomorphism in Id.run_seqLeft#12936

Merged
TwoFX merged 2 commits intoleanprover:masterfrom
eric-wieser:patch-72
Mar 17, 2026
Merged

fix: remove accidental type monomorphism in Id.run_seqLeft#12936
TwoFX merged 2 commits intoleanprover:masterfrom
eric-wieser:patch-72

Conversation

@eric-wieser
Copy link
Copy Markdown
Contributor

@eric-wieser eric-wieser commented Mar 16, 2026

This PR fixes Id.run_seqLeft and Id.run_seqRight to apply when the two monad results are different.

This PR fixes `Id.run_seqLeft` and `Id.run_seqRight` to apply when the two monad results are different.
@eric-wieser
Copy link
Copy Markdown
Contributor Author

changelog-library

@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Mar 16, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c685465bd442d278f26997393464bcd8c87062b --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-17 00:37:22)

@leanprover-bot
Copy link
Copy Markdown
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 5c685465bd442d278f26997393464bcd8c87062b --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-17 00:37:24)

Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Mar 17, 2026
Merged via the queue into leanprover:master with commit 6714601 Mar 17, 2026
18 of 19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library 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