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

Equations

• ts.toWallTime offset = Std.Time.WallTime.ofDuration (ts.val + Std.Time.Duration.ofSeconds offset.second)

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

Equations

• Std.Time.Timestamp.ofWallTime wt offset = Std.Time.Timestamp.ofDurationSinceUnixEpoch (wt.val - Std.Time.Duration.ofSeconds offset.second)

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

Equations

• wt.toTimestamp offset = Std.Time.Timestamp.ofWallTime wt 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.

Equations

• Std.Time.WallTime.ofTimestamp ts offset = ts.toWallTime offset

@[inline]

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

Converts a PlainDate to a WallTime.

Equations

• pd.toWallTime = Std.Time.WallTime.ofSeconds pd.toEpochDay.toSeconds

@[inline]

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

Converts a WallTime to a PlainDate.

Equations

• Std.Time.PlainDate.ofWallTime wt = Std.Time.PlainDate.ofEpochDay wt.toDays

@[implicit_reducible]

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

Equations

• Std.Time.PlainDate.instHSubDuration = { hSub := fun (x y : Std.Time.PlainDate) => x.toWallTime - y.toWallTime }

@[inline]

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

Converts a PlainTime to a WallTime.

Equations

• pt.toWallTime = Std.Time.WallTime.ofNanoseconds pt.toNanoseconds

@[inline]

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

Converts a WallTime to a PlainTime.

Equations

• Std.Time.PlainTime.ofWallTime wt = Std.Time.PlainTime.ofNanoseconds wt.toNanoseconds

@[inline]

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

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

Equations

• Std.Time.PlainDateTime.ofPlainDate date = { date := date, time := Std.Time.PlainTime.midnight }

@[inline]

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

Extracts the PlainDate component from a PlainDateTime.

Equations

• pdt.toPlainDate = pdt.date

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

Equations

• Std.Time.PlainDateTime.ofPlainTime time = { date := { year := 1, month := 1, day := 1, valid := Std.Time.PlainDateTime.ofPlainTime._proof_1✝ }, time := time }

@[inline]

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

Extracts the PlainTime component from a PlainDateTime.

Equations

• pdt.toPlainTime = pdt.time

@[implicit_reducible]

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

Equations

• Std.Time.PlainDateTime.instHSubDuration = { hSub := fun (x y : Std.Time.PlainDateTime) => x.toWallTime - y.toWallTime }