Skip to content
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

feat: add decidable instances for comparison operations of time offset types #6587

Merged
merged 4 commits into from
Jan 10, 2025
Merged

feat: add decidable instances for comparison operations of time offset types #6587

merged 4 commits into from
Jan 10, 2025

Conversation

algebraic-dev
Copy link
Contributor

@algebraic-dev algebraic-dev commented Jan 9, 2025 •
edited by TwoFX
Loading

This PR adds decidable instances for the LE and LT instances for the Offset types defined in Std.Time.

@algebraic-dev algebraic-dev requested a review from TwoFX as a code owner January 9, 2025 02:31
@algebraic-dev algebraic-dev self-assigned this Jan 9, 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 Jan 9, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 9, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0afa1d1e5dda3cfedd4a847421271fef64e9743c --onto 00ef231a6e03398c2ad3b577ab036f901ec88543. (2025-01-09 02:54:59)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0afa1d1e5dda3cfedd4a847421271fef64e9743c --onto dd6445515ddc71826c76b8020fe9e030579b432b. (2025-01-09 18:31:02)

TwoFX
TwoFX reviewed Jan 9, 2025
View reviewed changes
Copy link
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.

Looks like the following are missing

  • Month.Offset
  • Week.Offset

@algebraic-dev algebraic-dev added the awaiting-review Waiting for someone to review the PR label Jan 9, 2025
@TwoFX TwoFX changed the title feat: add decidable instances for all the time units feat: add decidable instances for comparison operation of time offset types Jan 10, 2025
@TwoFX TwoFX added this pull request to the merge queue Jan 10, 2025
@TwoFX TwoFX changed the title feat: add decidable instances for comparison operation of time offset types feat: add decidable instances for comparison operations of time offset types Jan 10, 2025
Merged via the queue into leanprover:master with commit ed309dc Jan 10, 2025
20 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@algebraic-dev @luisacicolini
feat: add decidable instances for comparison operation of time offset…
46aae0f 
… types (leanprover#6587)

This PR adds decidable instances for the `LE` and `LT` instances for the
`Offset` types defined in `Std.Time`.
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@algebraic-dev @JovanGerb
feat: add decidable instances for comparison operation of time offset…
dda76bd 
… types (leanprover#6587)

This PR adds decidable instances for the `LE` and `LT` instances for the
`Offset` types defined in `Std.Time`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

Assignees

@algebraic-dev algebraic-dev

Labels
awaiting-review Waiting for someone to review the 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.
3 participants
@algebraic-dev @leanprover-community-bot @TwoFX