fix: adjustments to the datetime library #6431
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
| @@ -28,9 +28,16 @@ structure PlainDateTime where | |||
| /-- | |||
| The `Time` component of a `PlainTime` | |||
| -/ | |||
| time : PlainTime | |||
| time : Sigma PlainTime | |||
There was a problem hiding this comment.
Did you consider also parameterizing PlainDateTime by leap as well?
|
|
||
| namespace PlainTime | ||
|
|
||
| /-- | ||
| Creates a `PlainTime` value representing midnight (00:00:00.000000000). | ||
| -/ | ||
| def midnight : PlainTime := | ||
| ⟨0, 0, ⟨true, 0⟩, 0⟩ | ||
| def midnight : PlainTime α := |
There was a problem hiding this comment.
What is the rational behind using α and not leap for this parameter in these definitions? It seems that a name of leap would be better when users wish to set it using named parameters,
| @@ -110,14 +111,14 @@ Converts a `PlainDate` to a `ZonedDateTime`. | |||
| -/ | |||
| @[inline] | |||
| def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := | |||
| ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) zr | |||
| ZonedDateTime.ofPlainDateTime (pd.atTime (α := true) PlainTime.midnight) zr | |||
There was a problem hiding this comment.
For example, these uses of (α := true) seem more readable as (leap := true).
| /-- | ||
| COMMENT | ||
| -/ | ||
| def LeapTime := PlainTime True |
There was a problem hiding this comment.
| def LeapTime := PlainTime True | |
| abbrev LeapTime := PlainTime True |
I imagine this is still TODO (given the COMMENT), but I imagine this definitely should be an abbrev rather than a def to inherit the instances of PlainTime.
| @@ -65,7 +65,7 @@ info: datetime("2000-01-19T03:02:01.000000000") | |||
| #guard_msgs in | |||
| #eval datetime - (1 : Day.Offset) | |||
|
|
|||
| def time := time("13:02:01") | |||
| def time : PlainTime true := time("13:02:01") | |||
There was a problem hiding this comment.
| def time : PlainTime true := time("13:02:01") | |
| def time : LeapTime := time("13:02:01") |
Maybe use this here and elsewhere (instead of PlainTime true)?
This PR fix some issues that I found while using the library and other things that some people suggested
Repr.LeapTimeand changedPlainTime : TypetoPlainType : (leap : Bool) -> Typereadlink -ftoIO.FS.realPath