diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index bf7b1dd9ef8d..fd40748d3853 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -44,7 +44,7 @@ def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp := Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos) /-- -Converts a UNIX `Timestamp` to a `PlainDateTime`. +Converts a `Timestamp` to a `PlainDateTime`. -/ def ofTimestamp (stamp : Timestamp) : PlainDateTime := Id.run do let leapYearEpoch := 11017