@[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.

@[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

@[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

@[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

@[inline]

def Std.Time.DateTime.toPlainDate {tz : TimeZone} (dt : DateTime tz) : PlainDate

Converts a DateTime to a PlainDate

Equations

• dt.toPlainDate = dt.toTimestamp.toPlainDateAssumingUTC

@[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

@[inline]

def Std.Time.DateTime.now {tz : TimeZone} : IO (DateTime tz)

Gets the current ZonedDateTime.

Equations

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

@[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)

@[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)

@[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

@[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)

@[inline]

def Std.Time.ZonedDateTime.toPlainDate (dt : ZonedDateTime) : PlainDate

Converts a ZonedDateTime to a PlainDate

Equations

• dt.toPlainDate = dt.toPlainDateTime.date

@[inline]

def Std.Time.ZonedDateTime.toPlainTime (dt : ZonedDateTime) : PlainTime

Converts a ZonedDateTime to a PlainTime

Equations

• dt.toPlainTime = dt.toPlainDateTime.time

@[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)

@[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

@[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

@[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

@[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