From 0fef367c9c5d22a744daba589f28a144bdc90ea3 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 5 Nov 2024 22:15:35 -0300 Subject: [PATCH] Update src/Std/Time/DateTime/PlainDateTime.lean Co-authored-by: Markus Himmel --- src/Std/Time/DateTime/PlainDateTime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index c9527dd1ae68..c87ce51b2fff 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