Skip to content

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Oct 17, 2025

This PR adds a missing move assignment operator, and deletes the copy assignment operator.

C++ types should not implement move constructors without also implementing move assignment. This also ensures that m_fn is correctly emptied after a move, which is not guaranteed by the standard.

This change is also needed to allow lean::optional to be eventually replaced by std::optional.

C++ types should not implement move constructors without also implementing move assignment.
This also ensures that m_fn is correctly emptied after a move
@eric-wieser
Copy link
Contributor Author

changelog-skip

@github-actions github-actions bot added changelog-skip toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Oct 17, 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 4077bf2c05b74a2eaaf1db9be957236f29614f63 --onto 4ce7ad19cea348506876685a19a7e0cca442c6d0. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-17 13:13:05)

@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 4077bf2c05b74a2eaaf1db9be957236f29614f63 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-17 13:13:07)

@TwoFX TwoFX added changelog-no Do not include this PR in the release changelog and removed changelog-skip labels Oct 20, 2025
@Kha Kha added this pull request to the merge queue Oct 21, 2025
Merged via the queue into leanprover:master with commit 3f82b30 Oct 21, 2025
35 of 42 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog 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.

5 participants