From ebf455a13780ea508abee8016b8bb6c5549bf9d7 Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 21 May 2025 10:04:36 +0200 Subject: [PATCH] doc: clarify that `.now` returns a date(time) in the local time zone (#8331) This PR improves the docstring for `PlainDateTime.now` and its variants. --------- Co-authored-by: Markus Himmel --- src/Std/Time/Zoned.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index 570007ce5e..efc4096fce 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -17,7 +17,8 @@ set_option linter.all true namespace PlainDateTime /-- -Get the current time. +Get the current time, in the local timezone. +To obtain the current time in a specific timezone, use `DateTime.now` or `ZonedDateTime.nowAt`. -/ @[inline] def now : IO PlainDateTime := do @@ -32,7 +33,7 @@ end PlainDateTime namespace PlainDate /-- -Get the current date. +Get the current date, in the local timezone. -/ @[inline] def now : IO PlainDate := @@ -42,7 +43,7 @@ end PlainDate namespace PlainTime /-- -Get the current time. +Get the current time, in the local timezone. -/ @[inline] def now : IO PlainTime :=