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

Datetime extension: Enable tests with negative timestamps #525

Open
1 of 2 tasks
adpaco-aws opened this issue Feb 4, 2025 · 0 comments
Open
1 of 2 tasks

Datetime extension: Enable tests with negative timestamps #525

adpaco-aws opened this issue Feb 4, 2025 · 0 comments
Labels
internal-improvement Refactoring, performance improvement, or other non-breaking change

Comments

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Feb 4, 2025 •
edited
Loading

Category

Lean formalization

Description

We encountered a bug in the datetime library when working on the testing in #519 . The bug is presumably fixed by leanprover/lean4#6668 so we'll be able to enable the commented out tests in #519 when we upgrade to a Lean version that includes the fix.

Is this something that you'd be interested in working on?

  • 👋 I may be able to implement this feature request
  • ⚠️ This feature might incur a breaking change
@adpaco-aws adpaco-aws added the internal-improvement Refactoring, performance improvement, or other non-breaking change label Feb 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
internal-improvement Refactoring, performance improvement, or other non-breaking change
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@adpaco-aws