@[inline]

def Std.Time.Timestamp.toWallTime (ts : Timestamp) (offset : TimeZone.Offset) : WallTime

Converts a Timestamp to a WallTime for a given timezone offset. The result is the local civil time: wall = UTC + offset.

@[inline]

def Std.Time.Timestamp.ofWallTime (wt : WallTime) (offset : TimeZone.Offset) : Timestamp

Creates a Timestamp from a WallTime and a timezone offset. Assumes the WallTime represents civil time at the given offset: UTC = wall − offset.

@[inline]

def Std.Time.WallTime.toTimestamp (wt : WallTime) (offset : TimeZone.Offset) : Timestamp

Converts a WallTime to a Timestamp given a timezone offset. The WallTime is treated as civil time at the given offset: UTC = wall − offset.

@[inline]

def Std.Time.WallTime.ofTimestamp (ts : Timestamp) (offset : TimeZone.Offset) : WallTime

Creates a WallTime from a Timestamp given a timezone offset. The result is the local civil time: wall = UTC + offset.

@[inline]

def Std.Time.PlainDate.toWallTime (pd : PlainDate) : WallTime

Converts a PlainDate to a WallTime.

@[inline]

def Std.Time.PlainDate.ofWallTime (wt : WallTime) : PlainDate

Converts a WallTime to a PlainDate.

@[implicit_reducible]

instance Std.Time.PlainDate.instHSubDuration : HSub PlainDate PlainDate Duration

@[inline]

def Std.Time.PlainTime.toWallTime (pt : PlainTime) : WallTime

Converts a PlainTime to a WallTime.

@[inline]

def Std.Time.PlainTime.ofWallTime (wt : WallTime) : PlainTime

Converts a WallTime to a PlainTime.

@[inline]

def Std.Time.PlainDateTime.ofPlainDate (date : PlainDate) : PlainDateTime

Wraps a PlainDate in a PlainDateTime with midnight as the time component.

@[inline]

def Std.Time.PlainDateTime.toPlainDate (pdt : PlainDateTime) : PlainDate

Extracts the PlainDate component from a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.ofPlainTime (time : PlainTime) : PlainDateTime

Wraps a PlainTime in a PlainDateTime with year 1, month 1, day 1 as the date component.

@[inline]

def Std.Time.PlainDateTime.toPlainTime (pdt : PlainDateTime) : PlainTime

Extracts the PlainTime component from a PlainDateTime.

@[implicit_reducible]

instance Std.Time.PlainDateTime.instHSubDuration : HSub PlainDateTime PlainDateTime Duration