structure Std.Time.DateTime (tz : TimeZone) : Type

Represents a specific point in time associated with a TimeZone.

• timestamp : Timestamp

  Timestamp represents the exact moment in time. It's a UTC related Timestamp.

• date : Thunk PlainDateTime

  Date is a Thunk containing the PlainDateTime that represents the local date and time, it's used for accessing data like day and month without having to recompute the data every time.

@[implicit_reducible]

instance Std.Time.instBEqDateTime {tz : TimeZone} : BEq (DateTime tz)

Equations

• Std.Time.instBEqDateTime = { beq := fun (x y : Std.Time.DateTime tz) => x.timestamp == y.timestamp }

@[implicit_reducible]

instance Std.Time.instOrdDateTime {tz : TimeZone} : Ord (DateTime tz)

Equations

• Std.Time.instOrdDateTime = { compare := compareOn fun (x : Std.Time.DateTime tz) => x.timestamp }

instance Std.Time.instTransOrdDateTime {tz : TimeZone} : TransOrd (DateTime tz)

instance Std.Time.instLawfulBEqOrdDateTime {tz : TimeZone} : LawfulBEqOrd (DateTime tz)

@[inline]

def Std.Time.DateTime.ofTimestamp (tm : Timestamp) (tz : TimeZone) : DateTime tz

Creates a new DateTime out of a Timestamp that is in a TimeZone.

Equations

• Std.Time.DateTime.ofTimestamp tm tz = { timestamp := tm, date := { fn := fun (x : Unit) => Std.Time.PlainDateTime.ofWallTime (Std.Time.WallTime.ofTimestamp tm tz.offset) } }

@[implicit_reducible]

instance Std.Time.DateTime.instInhabited {tz : TimeZone} : Inhabited (DateTime tz)

Equations

• Std.Time.DateTime.instInhabited = { default := Std.Time.DateTime.ofTimestamp default tz }

def Std.Time.DateTime.toEpochDay {tz : TimeZone} (date : DateTime tz) : Day.Offset

Returns the number of days since the UNIX epoch.

Equations

• date.toEpochDay = date.date.get.toEpochDay

@[inline]

def Std.Time.DateTime.toTimestamp {tz : TimeZone} (date : DateTime tz) : Timestamp

Creates a Timestamp out of a DateTime.

Equations

• date.toTimestamp = date.timestamp

@[inline]

def Std.Time.DateTime.convertTimeZone {tz : TimeZone} (date : DateTime tz) (tz₁ : TimeZone) : DateTime tz₁

Changes the TimeZone to a new one.

Equations

• date.convertTimeZone tz₁ = Std.Time.DateTime.ofTimestamp date.timestamp tz₁

@[inline]

def Std.Time.DateTime.ofPlainDateTime (date : PlainDateTime) (tz : TimeZone) : DateTime tz

Creates a new DateTime out of a PlainDateTime. It assumes that the PlainDateTime is the Local date time.

Equations

• Std.Time.DateTime.ofPlainDateTime date tz = { timestamp := Std.Time.Timestamp.ofWallTime date.toWallTime tz.offset, date := { fn := fun (x : Unit) => date } }

@[inline]

def Std.Time.DateTime.addHours {tz : TimeZone} (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz

Add Hour.Offset to a DateTime.

Equations

• dt.addHours hours = Std.Time.DateTime.ofTimestamp (dt.timestamp + hours) tz

@[inline]

def Std.Time.DateTime.subHours {tz : TimeZone} (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz

Subtract Hour.Offset from a DateTime.

Equations

• dt.subHours hours = Std.Time.DateTime.ofTimestamp (dt.timestamp - hours) tz

@[inline]

def Std.Time.DateTime.addMinutes {tz : TimeZone} (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz

Add Minute.Offset to a DateTime.

Equations

• dt.addMinutes minutes = Std.Time.DateTime.ofTimestamp (dt.timestamp + minutes) tz

@[inline]

def Std.Time.DateTime.subMinutes {tz : TimeZone} (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz

Subtract Minute.Offset from a DateTime.

Equations

• dt.subMinutes minutes = Std.Time.DateTime.ofTimestamp (dt.timestamp - minutes) tz

@[inline]

def Std.Time.DateTime.addSeconds {tz : TimeZone} (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz

Add Second.Offset to a DateTime.

Equations

• dt.addSeconds seconds = Std.Time.DateTime.ofTimestamp (dt.timestamp + seconds) tz

@[inline]

def Std.Time.DateTime.subSeconds {tz : TimeZone} (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz

Subtract Second.Offset from a DateTime.

Equations

• dt.subSeconds seconds = Std.Time.DateTime.ofTimestamp (dt.timestamp - seconds) tz

@[inline]

def Std.Time.DateTime.addMilliseconds {tz : TimeZone} (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz

Add Millisecond.Offset to a DateTime.

Equations

• dt.addMilliseconds milliseconds = Std.Time.DateTime.ofTimestamp (dt.timestamp + milliseconds) tz

@[inline]

def Std.Time.DateTime.subMilliseconds {tz : TimeZone} (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz

Subtract Millisecond.Offset from a DateTime.

Equations

• dt.subMilliseconds milliseconds = Std.Time.DateTime.ofTimestamp (dt.timestamp - milliseconds) tz

@[inline]

def Std.Time.DateTime.addNanoseconds {tz : TimeZone} (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz

Add Nanosecond.Offset to a DateTime.

Equations

• dt.addNanoseconds nanoseconds = Std.Time.DateTime.ofTimestamp (dt.timestamp + nanoseconds) tz

@[inline]

def Std.Time.DateTime.subNanoseconds {tz : TimeZone} (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz

Subtract Nanosecond.Offset from a DateTime.

Equations

• dt.subNanoseconds nanoseconds = Std.Time.DateTime.ofTimestamp (dt.timestamp - nanoseconds) tz

@[inline]

def Std.Time.DateTime.addDays {tz : TimeZone} (dt : DateTime tz) (days : Day.Offset) : DateTime tz

Add Day.Offset to a DateTime.

Equations

• dt.addDays days = Std.Time.DateTime.ofTimestamp (dt.timestamp + days) tz

@[inline]

def Std.Time.DateTime.subDays {tz : TimeZone} (dt : DateTime tz) (days : Day.Offset) : DateTime tz

Subtracts Day.Offset to a DateTime.

Equations

• dt.subDays days = Std.Time.DateTime.ofTimestamp (dt.timestamp - days) tz

@[inline]

def Std.Time.DateTime.addWeeks {tz : TimeZone} (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz

Add Week.Offset to a DateTime.

Equations

• dt.addWeeks weeks = Std.Time.DateTime.ofTimestamp (dt.timestamp + weeks) tz

@[inline]

def Std.Time.DateTime.subWeeks {tz : TimeZone} (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz

Subtracts Week.Offset to a DateTime.

Equations

• dt.subWeeks weeks = Std.Time.DateTime.ofTimestamp (dt.timestamp - weeks) tz

def Std.Time.DateTime.addMonthsClip {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Add Month.Offset to a DateTime, it clips the day to the last valid day of that month.

Equations

• dt.addMonthsClip months = Std.Time.DateTime.ofPlainDateTime (dt.date.get.addMonthsClip months) tz

@[inline]

def Std.Time.DateTime.subMonthsClip {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Subtracts Month.Offset from a DateTime, it clips the day to the last valid day of that month.

Equations

• dt.subMonthsClip months = Std.Time.DateTime.ofPlainDateTime (dt.date.get.subMonthsClip months) tz

def Std.Time.DateTime.addMonthsRollOver {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Add Month.Offset from a DateTime, this function rolls over any excess days into the following month.

Equations

• dt.addMonthsRollOver months = Std.Time.DateTime.ofPlainDateTime (dt.date.get.addMonthsRollOver months) tz

@[inline]

def Std.Time.DateTime.subMonthsRollOver {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Subtract Month.Offset from a DateTime, this function rolls over any excess days into the following month.

Equations

• dt.subMonthsRollOver months = Std.Time.DateTime.ofPlainDateTime (dt.date.get.subMonthsRollOver months) tz

@[inline]

def Std.Time.DateTime.addYearsRollOver {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Add Year.Offset to a DateTime, this function rolls over any excess days into the following month.

Equations

• dt.addYearsRollOver years = Std.Time.DateTime.ofPlainDateTime (dt.date.get.addYearsRollOver years) tz

@[inline]

def Std.Time.DateTime.addYearsClip {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Add Year.Offset to a DateTime, it clips the day to the last valid day of that month.

Equations

• dt.addYearsClip years = Std.Time.DateTime.ofPlainDateTime (dt.date.get.addYearsClip years) tz

@[inline]

def Std.Time.DateTime.subYearsRollOver {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Subtract Year.Offset from a DateTime, this function rolls over any excess days into the following month.

Equations

• dt.subYearsRollOver years = Std.Time.DateTime.ofPlainDateTime (dt.date.get.subYearsRollOver years) tz

@[inline]

def Std.Time.DateTime.subYearsClip {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Subtract Year.Offset from to a DateTime, it clips the day to the last valid day of that month.

Equations

• dt.subYearsClip years = Std.Time.DateTime.ofPlainDateTime (dt.date.get.subYearsClip years) tz

@[inline]

def Std.Time.DateTime.withDaysClip {tz : TimeZone} (dt : DateTime tz) (days : Day.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the day of the month to the given days value, with any out-of-range days clipped to the nearest valid date.

Equations

• dt.withDaysClip days = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withDaysClip days) tz

@[inline]

def Std.Time.DateTime.withDaysRollOver {tz : TimeZone} (dt : DateTime tz) (days : Day.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the day of the month to the given days value, with any out-of-range days rolled over to the next month or year as needed.

Equations

• dt.withDaysRollOver days = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withDaysRollOver days) tz

@[inline]

def Std.Time.DateTime.withMonthClip {tz : TimeZone} (dt : DateTime tz) (month : Month.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the month to the given month value. The day remains unchanged, and any invalid days for the new month will be handled according to the clip behavior.

Equations

• dt.withMonthClip month = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withMonthClip month) tz

@[inline]

def Std.Time.DateTime.withMonthRollOver {tz : TimeZone} (dt : DateTime tz) (month : Month.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the month to the given month value. The day is rolled over to the next valid month if necessary.

Equations

• dt.withMonthRollOver month = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withMonthRollOver month) tz

@[inline]

def Std.Time.DateTime.withYearClip {tz : TimeZone} (dt : DateTime tz) (year : Year.Offset) : DateTime tz

Creates a new DateTime tz by adjusting the year to the given year value. The month and day remain unchanged, and any invalid days for the new year will be handled according to the clip behavior.

Equations

• dt.withYearClip year = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withYearClip year) tz

@[inline]

def Std.Time.DateTime.withYearRollOver {tz : TimeZone} (dt : DateTime tz) (year : Year.Offset) : DateTime tz

Creates a new DateTime tz by adjusting the year to the given year value. The month and day are rolled over to the next valid month and day if necessary.

Equations

• dt.withYearRollOver year = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withYearRollOver year) tz

@[inline]

def Std.Time.DateTime.withHours {tz : TimeZone} (dt : DateTime tz) (hour : Hour.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the hour component.

Equations

• dt.withHours hour = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withHours hour) tz

@[inline]

def Std.Time.DateTime.withMinutes {tz : TimeZone} (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the minute component.

Equations

• dt.withMinutes minute = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withMinutes minute) tz

@[inline]

def Std.Time.DateTime.withSeconds {tz : TimeZone} (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz

Creates a new DateTime tz by adjusting the second component.

Equations

• dt.withSeconds second = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withSeconds second) tz

@[inline]

def Std.Time.DateTime.withNanoseconds {tz : TimeZone} (dt : DateTime tz) (nano : Nanosecond.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the nano component.

Equations

• dt.withNanoseconds nano = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withNanoseconds nano) tz

@[inline]

def Std.Time.DateTime.withMilliseconds {tz : TimeZone} (dt : DateTime tz) (milli : Millisecond.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the millisecond component.

Equations

• dt.withMilliseconds milli = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withMilliseconds milli) tz

@[inline]

def Std.Time.DateTime.toPlainDateTime {tz : TimeZone} (dt : DateTime tz) : PlainDateTime

Converts a Timestamp to a PlainDateTime

Equations

• dt.toPlainDateTime = dt.date.get

@[inline]

def Std.Time.DateTime.year {tz : TimeZone} (dt : DateTime tz) : Year.Offset

Getter for the Year inside of a DateTime

Equations

• dt.year = dt.date.get.year

@[inline]

def Std.Time.DateTime.month {tz : TimeZone} (dt : DateTime tz) : Month.Ordinal

Getter for the Month inside of a DateTime

Equations

• dt.month = dt.date.get.month

@[inline]

def Std.Time.DateTime.day {tz : TimeZone} (dt : DateTime tz) : Day.Ordinal

Getter for the Day inside of a DateTime

Equations

• dt.day = dt.date.get.day

@[inline]

def Std.Time.DateTime.hour {tz : TimeZone} (dt : DateTime tz) : Hour.Ordinal

Getter for the Hour inside of a DateTime

Equations

• dt.hour = dt.date.get.hour

@[inline]

def Std.Time.DateTime.minute {tz : TimeZone} (dt : DateTime tz) : Minute.Ordinal

Getter for the Minute inside of a DateTime

Equations

• dt.minute = dt.date.get.minute

@[inline]

def Std.Time.DateTime.second {tz : TimeZone} (dt : DateTime tz) : Second.Ordinal true

Getter for the Second inside of a DateTime

Equations

• dt.second = dt.date.get.second

@[inline]

def Std.Time.DateTime.millisecond {tz : TimeZone} (dt : DateTime tz) : Millisecond.Ordinal

Getter for the Milliseconds inside of a DateTime

Equations

• dt.millisecond = Std.Time.Internal.Bounded.LE.emod dt.date.get.time.nanosecond 1000 Std.Time.DateTime.millisecond._proof_1✝

@[inline]

def Std.Time.DateTime.nanosecond {tz : TimeZone} (dt : DateTime tz) : Nanosecond.Ordinal

Getter for the Nanosecond inside of a DateTime

Equations

• dt.nanosecond = dt.date.get.time.nanosecond

@[inline]

def Std.Time.DateTime.weekday {tz : TimeZone} (dt : DateTime tz) : Weekday

Gets the Weekday of a DateTime.

def Std.Time.DateTime.era {tz : TimeZone} (date : DateTime tz) : Year.Era

Determines the era of the given DateTime based on its year.

Equations

• date.era = date.year.era

def Std.Time.DateTime.withWeekday {tz : TimeZone} (dt : DateTime tz) (desiredWeekday : Weekday) : DateTime tz

Sets the DateTime to the specified desiredWeekday.

Equations

• dt.withWeekday desiredWeekday = Std.Time.DateTime.ofPlainDateTime (dt.date.get.withWeekday desiredWeekday) tz

def Std.Time.DateTime.inLeapYear {tz : TimeZone} (date : DateTime tz) : Bool

Checks if the DateTime is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

def Std.Time.DateTime.dayOfYear {tz : TimeZone} (date : DateTime tz) : Day.Ordinal.OfYear date.year.isLeap

Determines the ordinal day of the year for the given DateTime.

Equations

• date.dayOfYear = Std.Time.ValidDate.dayOfYear ⟨(date.month, date.day), ⋯⟩

@[inline]

def Std.Time.DateTime.weekOfYear {tz : TimeZone} (date : DateTime tz) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

Determines the week of the year for the given DateTime, using firstDay as the start of the week.

Equations

• date.weekOfYear firstDay = date.date.get.weekOfYear firstDay

@[inline]

def Std.Time.DateTime.weekYear {tz : TimeZone} (date : DateTime tz) (firstDay : Weekday := Weekday.monday) : Year.Offset

Returns the week-based year for the given DateTime, using firstDay as the start of the week. The week-based year may differ from the calendar year for dates near the start or end of the year.

Equations

• date.weekYear firstDay = date.date.get.weekYear firstDay

def Std.Time.DateTime.weekOfMonth {tz : TimeZone} (date : DateTime tz) : Internal.Bounded.LE 1 5

Returns the unaligned week of the month for a DateTime (day divided by 7, plus 1).

Equations

• date.weekOfMonth = date.date.get.weekOfMonth

@[inline]

def Std.Time.DateTime.alignedWeekOfMonth {tz : TimeZone} (date : DateTime tz) (firstDay : Weekday := Weekday.monday) : Week.Ordinal.OfMonth

Determines the week of the month for the given DateTime, using firstDay as the start of the week.

Equations

• date.alignedWeekOfMonth firstDay = date.date.get.alignedWeekOfMonth firstDay

@[inline]

def Std.Time.DateTime.quarter {tz : TimeZone} (date : DateTime tz) : Internal.Bounded.LE 1 4

Determines the quarter of the year for the given DateTime.

Equations

• date.quarter = date.date.get.quarter

@[inline]

def Std.Time.DateTime.time {tz : TimeZone} (zdt : DateTime tz) : PlainTime

Getter for the PlainTime inside of a DateTime

Equations

• zdt.time = zdt.date.get.time

@[inline]

def Std.Time.DateTime.ofEpochDay (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz

Creates a DateTime from a number of days since the 1970-01-01T00:00:00.

Equations

• Std.Time.DateTime.ofEpochDay days time tz = Std.Time.DateTime.ofPlainDateTime (Std.Time.PlainDateTime.ofEpochDay days time) tz

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset {tz : TimeZone} : HAdd (DateTime tz) Day.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset = { hAdd := Std.Time.DateTime.addDays }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset {tz : TimeZone} : HSub (DateTime tz) Day.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset = { hSub := Std.Time.DateTime.subDays }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_1 {tz : TimeZone} : HAdd (DateTime tz) Week.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_1 = { hAdd := Std.Time.DateTime.addWeeks }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_1 {tz : TimeZone} : HSub (DateTime tz) Week.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_1 = { hSub := Std.Time.DateTime.subWeeks }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_2 {tz : TimeZone} : HAdd (DateTime tz) Hour.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_2 = { hAdd := Std.Time.DateTime.addHours }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_2 {tz : TimeZone} : HSub (DateTime tz) Hour.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_2 = { hSub := Std.Time.DateTime.subHours }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_3 {tz : TimeZone} : HAdd (DateTime tz) Minute.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_3 = { hAdd := Std.Time.DateTime.addMinutes }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_3 {tz : TimeZone} : HSub (DateTime tz) Minute.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_3 = { hSub := Std.Time.DateTime.subMinutes }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_4 {tz : TimeZone} : HAdd (DateTime tz) Second.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_4 = { hAdd := Std.Time.DateTime.addSeconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_4 {tz : TimeZone} : HSub (DateTime tz) Second.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_4 = { hSub := Std.Time.DateTime.subSeconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_5 {tz : TimeZone} : HAdd (DateTime tz) Millisecond.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_5 = { hAdd := Std.Time.DateTime.addMilliseconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_5 {tz : TimeZone} : HSub (DateTime tz) Millisecond.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_5 = { hSub := Std.Time.DateTime.subMilliseconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_6 {tz : TimeZone} : HAdd (DateTime tz) Nanosecond.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHAddOffset_6 = { hAdd := Std.Time.DateTime.addNanoseconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_6 {tz : TimeZone} : HSub (DateTime tz) Nanosecond.Offset (DateTime tz)

Equations

• Std.Time.DateTime.instHSubOffset_6 = { hSub := Std.Time.DateTime.subNanoseconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubDuration {tz tz₁ : TimeZone} : HSub (DateTime tz) (DateTime tz₁) Duration

Equations

• Std.Time.DateTime.instHSubDuration = { hSub := fun (x : Std.Time.DateTime tz) (y : Std.Time.DateTime tz₁) => x.toTimestamp - y.toTimestamp }

@[implicit_reducible]

instance Std.Time.DateTime.instHAddDuration {tz : TimeZone} : HAdd (DateTime tz) Duration (DateTime tz)

Equations

• Std.Time.DateTime.instHAddDuration = { hAdd := fun (x : Std.Time.DateTime tz) (y : Std.Time.Duration) => x.addNanoseconds y.toNanoseconds }

@[implicit_reducible]

instance Std.Time.DateTime.instHSubDuration_1 {tz : TimeZone} : HSub (DateTime tz) Duration (DateTime tz)

Equations

• Std.Time.DateTime.instHSubDuration_1 = { hSub := fun (x : Std.Time.DateTime tz) (y : Std.Time.Duration) => x.subNanoseconds y.toNanoseconds }