@[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 DateTime.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.now : IO DateTime

Gets the current DateTime.

Equations

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

@[inline]

def Std.Time.DateTime.nowAt (id : String) : IO DateTime

Gets the current DateTime using the identifier of a time zone.

Equations

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

@[inline]

def Std.Time.DateTime.ofLocalDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : DateTime

Converts a PlainDate to a DateTime.

Equations

• Std.Time.DateTime.ofLocalDate pd zr = Std.Time.DateTime.ofPlainDateTime (pd.atTime Std.Time.PlainTime.midnight) zr

@[inline]

def Std.Time.DateTime.ofLocalDateWithZone (pd : PlainDate) (zr : TimeZone) : DateTime

Converts a PlainDate to a DateTime using TimeZone.

Equations

• Std.Time.DateTime.ofLocalDateWithZone pd zr = Std.Time.DateTime.ofPlainDateTime (pd.atTime Std.Time.PlainTime.midnight) (Std.Time.TimeZone.ZoneRules.ofTimeZone zr)

@[inline]

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

Converts a DateTime to a PlainDate

Equations

• dt.toPlainDate = dt.toPlainDateTime.date

@[inline]

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

Converts a DateTime to a PlainTime

Equations

• dt.toPlainTime = dt.toPlainDateTime.time

@[inline]

def Std.Time.DateTime.of (pdt : PlainDateTime) (id : String) : IO DateTime

Creates a new DateTime out of a PlainDateTime and a time zone identifier.

Equations

• Std.Time.DateTime.of pdt id = do let zr ← Std.Time.Database.defaultGetZoneRules id pure (Std.Time.DateTime.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.DateTime.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.DateTime.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.DateTime.ofLocalDate 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.DateTime.ofLocalDateWithZone dt tz).toTimestamp