Skip to content

Commit

Permalink
feat: update proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
bergmannjg committed Jan 11, 2025
1 parent f6f88b9 commit 10a03bf
Show file tree
Hide file tree
Showing 6 changed files with 159 additions and 127 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# PlainDate.ofDaysSinceUNIXEpoch is a valid date

[Proof](https://github.com/bergmannjg/Std.Time.Lemmas/blob/main/Time/Date/Lemmas.lean#L800) that
[Proof](https://github.com/bergmannjg/Std.Time.Lemmas/blob/main/Time/Date/Lemmas.lean#L834) that
[PlainDate.ofDaysSinceUNIXEpoch](https://github.com/leanprover/lean4/blob/v4.15.0-rc1/src/Std/Time/Date/PlainDate.lean#L79) gives a valid
[PlainDate](https://github.com/leanprover/lean4/blob/v4.15.0-rc1/src/Std/Time/Date/PlainDate.lean#L24).
Loading

0 comments on commit 10a03bf

Please sign in to comment.