Skip to content

fix: correct swapped operands in Std.Time subtraction instances#12919

Merged
TwoFX merged 1 commit intoleanprover:masterfrom
jessealama:fix/time-sub-bugs
Mar 16, 2026
Merged

fix: correct swapped operands in Std.Time subtraction instances#12919
TwoFX merged 1 commit intoleanprover:masterfrom
jessealama:fix/time-sub-bugs

Conversation

@jessealama
Copy link
Copy Markdown
Contributor

This PR fixes the HSub PlainTime Duration instance, which had its operands reversed: it computed duration - time instead of time - duration. For example, subtracting 2 minutes from time("13:02:01") would give time("10:57:59") rather than the expected time("13:00:01"). We also noticed that HSub PlainDateTime Millisecond.Offset is similarly affected.

Closes #12918

@jessealama jessealama requested a review from TwoFX as a code owner March 14, 2026 13:36
@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 Mar 14, 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 c2d4079193fa62cbd177059d9022c7a7ae097c42 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-14 15:20:19)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 14, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c2d4079193fa62cbd177059d9022c7a7ae097c42 --onto 47b3be05247c1d749f7031c06405ddc86daa4b09. You can force reference manual CI using the force-manual-ci label. (2026-03-14 15:20:21)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-09 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. (2026-03-14 22:12:22)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 14, 2026
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 14, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 14, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 14, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

@TwoFX TwoFX added the changelog-library Library label Mar 16, 2026
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 16, 2026
Merged via the queue into leanprover:master with commit fa9a32b Mar 16, 2026
28 of 30 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

Std.Time: some subtraction instances swap order of operations

3 participants