Skip to content

feat: LawfulMonad and WPMonad instances for Option and OptionT #9932

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
sgraf812 merged 1 commit into from
Oct 1, 2025
Merged

feat: LawfulMonad and WPMonad instances for Option and OptionT #9932

sgraf812 merged 1 commit into from
Oct 1, 2025

Conversation

@sgraf812
Copy link
Contributor

@sgraf812 sgraf812 commented Aug 15, 2025

This PR adds LawfulMonad and WPMonad instances for Option and OptionT.

@sgraf812 sgraf812 added the changelog-library Library label Aug 15, 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 Aug 15, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Aug 15, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-08-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-08-15 18:46:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4338a8be32df2d1ec54057945cd4221845a3cc46 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-29 08:37:13)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-29 10:32:22)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-01 15:26:21)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 15, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9932
1811271
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 15, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9932
e8e0010
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Aug 15, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Aug 15, 2025 •
edited
Loading

Mathlib CI status (docs):

@sgraf812 sgraf812 force-pushed the sg/wp-option branch 3 times, most recently from 7105f8b to 5fca174 Compare September 29, 2025 09:23
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
89fc732
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
da65ad6
@sgraf812 sgraf812 force-pushed the sg/wp-option branch 2 times, most recently from 80681d7 to 1c79aac Compare September 29, 2025 14:07
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
ddc76a9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
196f322
@sgraf812 sgraf812 marked this pull request as draft September 30, 2025 15:20
@sgraf812 sgraf812 closed this Sep 30, 2025
@sgraf812 sgraf812 reopened this Sep 30, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
e5f27d9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
6d02d76
@sgraf812 sgraf812 marked this pull request as ready for review October 1, 2025 12:26
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR labels Oct 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
85d16d6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9932
07d3833
@sgraf812 sgraf812 added this pull request to the merge queue Oct 1, 2025
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 1, 2025
Merged via the queue into master with commit ba52e93 Oct 1, 2025
20 checks passed
@sgraf812 sgraf812 deleted the sg/wp-option branch October 1, 2025 16:58
arthur-adjedj pushed a commit to arthur-adjedj/lean4 that referenced this pull request Oct 6, 2025
@sgraf812 @arthur-adjedj
feat: LawfulMonad and WPMonad instances for Option and OptionT (
9fafcf5 
leanprover#9932)

This PR adds `LawfulMonad` and `WPMonad` instances for `Option` and
`OptionT`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@sgraf812 @leanprover-bot @leanprover-community-bot