@[inline]

def Std.Time.Timestamp.ofPlainDateTimeAssumingUTC (pdt : PlainDateTime) : Timestamp

Converts a PlainDateTime to a Timestamp

Equations

• Std.Time.Timestamp.ofPlainDateTimeAssumingUTC pdt = pdt.toTimestampAssumingUTC

@[inline]

def Std.Time.Timestamp.toPlainDateTimeAssumingUTC (timestamp : Timestamp) : PlainDateTime

Converts a Timestamp to a PlainDateTime

Equations

• timestamp.toPlainDateTimeAssumingUTC = Std.Time.PlainDateTime.ofTimestampAssumingUTC timestamp

@[inline]

def Std.Time.Timestamp.ofPlainDateAssumingUTC (pd : PlainDate) : Timestamp

Converts a PlainDate to a Timestamp

Equations

• Std.Time.Timestamp.ofPlainDateAssumingUTC pd = Std.Time.Timestamp.ofSecondsSinceUnixEpoch pd.toDaysSinceUNIXEpoch.toSeconds

@[inline]

def Std.Time.Timestamp.toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate

Converts a Timestamp to a PlainDate

Equations

• timestamp.toPlainDateAssumingUTC = Std.Time.PlainDate.ofDaysSinceUNIXEpoch (Std.Time.Day.Offset.ofSeconds timestamp.toSecondsSinceUnixEpoch)

@[inline]

def Std.Time.Timestamp.getTimeAssumingUTC (timestamp : Timestamp) : PlainTime

Converts a Timestamp to a PlainTime

Equations

• timestamp.getTimeAssumingUTC = Std.Time.PlainTime.ofNanoseconds timestamp.toNanosecondsSinceUnixEpoch

@[inline]

def Std.Time.PlainDate.toTimestampAssumingUTC (pdt : PlainDate) : Timestamp

Converts a PlainDate to a Timestamp

Equations

• pdt.toTimestampAssumingUTC = Std.Time.Timestamp.ofPlainDateAssumingUTC pdt

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

Equations

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

@[inline]

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

Converts a PlainDate to a Timestamp

Equations

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

@[inline]

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

Converts a PlainDateTime to a PlainDate

Equations

• pdt.toPlainDate = pdt.date

@[inline]

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

Converts a PlainTime to a PlainDateTime

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

Converts a PlainDateTime to a PlainTime

Equations

• pdt.toPlainTime = pdt.time

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

Equations

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