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 <markus@lean-fro.org>
This commit is contained in:
parent
87cc330489
commit
ebf455a137
1 changed files with 4 additions and 3 deletions
|
|
@ -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 :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue