source
@[inline]
def Std.Time.PlainDateTime.now :
IO PlainDateTime

Get the current time, in the local timezone. To obtain the current time in a specific timezone, use `DateTime.now` or `ZonedDateTime.nowAt`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def Std.Time.PlainDate.now :
IO PlainDate

Get the current date, in the local timezone.

Equations

- Std.Time.PlainDate.now = Std.Time.PlainDateTime.date <$> Std.Time.PlainDateTime.now

Instances For

source
@[inline]
def Std.Time.PlainTime.now :
IO PlainTime

Get the current time, in the local timezone.

Equations

- Std.Time.PlainTime.now = Std.Time.PlainDateTime.time <$> Std.Time.PlainDateTime.now

Instances For

source
@[inline]
def Std.Time.DateTime.ofPlainDate (pd : PlainDate) (tz : TimeZone) :
DateTime tz

Converts a `PlainDate` with a `TimeZone` to a `DateTime`

Equations

- Std.Time.DateTime.ofPlainDate pd tz = Std.Time.DateTime.ofTimestamp (Std.Time.Timestamp.ofPlainDateAssumingUTC pd) tz

Instances For

source
@[inline]
def Std.Time.DateTime.toPlainDate {tz : TimeZone} (dt : DateTime tz) :
PlainDate

Converts a `DateTime` to a `PlainDate`

Equations

- dt.toPlainDate = dt.toTimestamp.toPlainDateAssumingUTC

Instances For

source
@[inline]
def Std.Time.DateTime.toPlainTime {tz : TimeZone} (dt : DateTime tz) :
PlainTime

Converts a `DateTime` to a `PlainTime`

Equations

- dt.toPlainTime = dt.date.get.time

Instances For

source
@[inline]
def Std.Time.DateTime.now {tz : TimeZone} :
IO (DateTime tz)

Gets the current `DateTime`.

Equations

- Std.Time.DateTime.now = do let tm ← Std.Time.Timestamp.now pure (Std.Time.DateTime.ofTimestamp tm tz)

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.now :
IO ZonedDateTime

Gets the current `ZonedDateTime`.

Equations

- Std.Time.ZonedDateTime.now = do let tm ← Std.Time.Timestamp.now let rules ← Std.Time.Database.defaultGetLocalZoneRules pure (Std.Time.ZonedDateTime.ofTimestamp tm rules)

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.nowAt (id : String) :
IO ZonedDateTime

Gets the current `ZonedDateTime` using the identifier of a time zone.

Equations

- Std.Time.ZonedDateTime.nowAt id = do let tm ← Std.Time.Timestamp.now let rules ← Std.Time.Database.defaultGetZoneRules id pure (Std.Time.ZonedDateTime.ofTimestamp tm rules)

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) :
ZonedDateTime

Converts a `PlainDate` to a `ZonedDateTime`.

Equations

- Std.Time.ZonedDateTime.ofPlainDate pd zr = Std.Time.ZonedDateTime.ofPlainDateTime (pd.atTime Std.Time.PlainTime.midnight) zr

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.ofPlainDateWithZone (pd : PlainDate) (zr : TimeZone) :
ZonedDateTime

Converts a `PlainDate` to a `ZonedDateTime` using `TimeZone`.

Equations

- Std.Time.ZonedDateTime.ofPlainDateWithZone pd zr = Std.Time.ZonedDateTime.ofPlainDateTime (pd.atTime Std.Time.PlainTime.midnight) (Std.Time.TimeZone.ZoneRules.ofTimeZone zr)

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.toPlainDate (dt : ZonedDateTime) :
PlainDate

Converts a `ZonedDateTime` to a `PlainDate`

Equations

- dt.toPlainDate = dt.toPlainDateTime.date

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.toPlainTime (dt : ZonedDateTime) :
PlainTime

Converts a `ZonedDateTime` to a `PlainTime`

Equations

- dt.toPlainTime = dt.toPlainDateTime.time

Instances For

source
@[inline]
def Std.Time.ZonedDateTime.of (pdt : PlainDateTime) (id : String) :
IO ZonedDateTime

Creates a new `ZonedDateTime` out of a `PlainDateTime` and a time zone identifier.

Equations

- Std.Time.ZonedDateTime.of pdt id = do let zr ← Std.Time.Database.defaultGetZoneRules id pure (Std.Time.ZonedDateTime.ofPlainDateTime pdt zr)

Instances For

source
@[inline]
def Std.Time.PlainDateTime.toTimestamp (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) :
Timestamp

Converts a `PlainDateTime` to a `Timestamp` using the `ZoneRules`.

Equations

- pdt.toTimestamp zr = (Std.Time.ZonedDateTime.ofPlainDateTime pdt zr).toTimestamp

Instances For

source
@[inline]
def Std.Time.PlainDateTime.toTimestampWithZone (pdt : PlainDateTime) (tz : TimeZone) :
Timestamp

Converts a `PlainDateTime` to a `Timestamp` using the `TimeZone`.

Equations

- pdt.toTimestampWithZone tz = (Std.Time.ZonedDateTime.ofPlainDateTimeWithZone pdt tz).toTimestamp

Instances For

source
@[inline]
def Std.Time.PlainDate.toTimestamp (dt : PlainDate) (zr : TimeZone.ZoneRules) :
Timestamp

Converts a `PlainDate` to a `Timestamp` using the `ZoneRules`.

Equations

- dt.toTimestamp zr = (Std.Time.ZonedDateTime.ofPlainDate dt zr).toTimestamp

Instances For

source
@[inline]
def Std.Time.PlainDate.toTimestampWithZone (dt : PlainDate) (tz : TimeZone) :
Timestamp

Converts a `PlainDate` to a `Timestamp` using the `TimeZone`.

Equations

- dt.toTimestampWithZone tz = (Std.Time.ZonedDateTime.ofPlainDateWithZone dt tz).toTimestamp

Instances For