Skip to content

Definitions#23

Merged
aria-eide merged 8 commits into
mainfrom
definitions
Nov 6, 2025
Merged

Definitions#23
aria-eide merged 8 commits into
mainfrom
definitions

Conversation

@voiestad
Copy link
Copy Markdown
Member

@voiestad voiestad commented Nov 5, 2025

Add definitions for:

  • 4.5.5 DifferenceTime
  • 4.5.8 RegulateTime
  • 8.5.5 AddInstant
  • 13.16 ToSecondsStringPrecisionRecord

Other stuff:

  • Fix missing primes in TimeDurationFromComponents. The mechanization was previously incorrect.
  • Shorten some proofs

@voiestad voiestad requested a review from aria-eide November 5, 2025 19:23
Copy link
Copy Markdown
Collaborator

@aria-eide aria-eide left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Beautiful!!

@aria-eide aria-eide merged commit 682af6f into main Nov 6, 2025
1 check passed
@aria-eide aria-eide deleted the definitions branch November 6, 2025 09:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants