Skip to content

Commit ebf455a

Browse files
grunwegTwoFX
andauthored
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 <[email protected]>
1 parent 87cc330 commit ebf455a

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/Std/Time/Zoned.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ set_option linter.all true
1717
namespace PlainDateTime
1818

1919
/--
20-
Get the current time.
20+
Get the current time, in the local timezone.
21+
To obtain the current time in a specific timezone, use `DateTime.now` or `ZonedDateTime.nowAt`.
2122
-/
2223
@[inline]
2324
def now : IO PlainDateTime := do
@@ -32,7 +33,7 @@ end PlainDateTime
3233
namespace PlainDate
3334

3435
/--
35-
Get the current date.
36+
Get the current date, in the local timezone.
3637
-/
3738
@[inline]
3839
def now : IO PlainDate :=
@@ -42,7 +43,7 @@ end PlainDate
4243
namespace PlainTime
4344

4445
/--
45-
Get the current time.
46+
Get the current time, in the local timezone.
4647
-/
4748
@[inline]
4849
def now : IO PlainTime :=

0 commit comments

Comments
 (0)