structure Std.Time.ZonedDateTime : Type

Represents a date and time with timezone information.

• date : Thunk PlainDateTime

  The plain datetime component, evaluated lazily.

• timestamp : Timestamp

  The corresponding timestamp for the datetime.

• rules : TimeZone.ZoneRules

  The timezone rules applied to this datetime.

• timezone : TimeZone

  The timezone associated with this datetime.

@[implicit_reducible]

instance Std.Time.instInhabitedZonedDateTime : Inhabited ZonedDateTime

Equations

• Std.Time.instInhabitedZonedDateTime = { default := Std.Time.instInhabitedZonedDateTime._private_1 }

@[inline]

def Std.Time.ZonedDateTime.ofTimestamp (tm : Timestamp) (rules : TimeZone.ZoneRules) : ZonedDateTime

Creates a new ZonedDateTime out of a Timestamp and a ZoneRules.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Time.ZonedDateTime.ofPlainDateTime (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) : ZonedDateTime

Creates a new ZonedDateTime out of a PlainDateTime and a ZoneRules. It assumes PlainDateTime is the local time.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Time.ZonedDateTime.ofTimestampWithZone (tm : Timestamp) (tz : TimeZone) : ZonedDateTime

Creates a new ZonedDateTime out of a Timestamp and a TimeZone.

Equations

• Std.Time.ZonedDateTime.ofTimestampWithZone tm tz = Std.Time.ZonedDateTime.ofTimestamp tm (Std.Time.TimeZone.ZoneRules.ofTimeZone tz)

@[inline]

def Std.Time.ZonedDateTime.ofPlainDateTimeWithZone (tm : PlainDateTime) (tz : TimeZone) : ZonedDateTime

Creates a new ZonedDateTime out of a PlainDateTime and a TimeZone. It assumes PlainDateTime is the local time.

Equations

• Std.Time.ZonedDateTime.ofPlainDateTimeWithZone tm tz = Std.Time.ZonedDateTime.ofPlainDateTime tm (Std.Time.TimeZone.ZoneRules.ofTimeZone tz)

@[inline]

def Std.Time.ZonedDateTime.toTimestamp (date : ZonedDateTime) : Timestamp

Creates a new Timestamp out of a ZonedDateTime.

Equations

• date.toTimestamp = date.timestamp

@[inline]

def Std.Time.ZonedDateTime.convertZoneRules (date : ZonedDateTime) (tz₁ : TimeZone.ZoneRules) : ZonedDateTime

Changes the ZoneRules to a new one.

Equations

• date.convertZoneRules tz₁ = Std.Time.ZonedDateTime.ofTimestamp date.toTimestamp tz₁

@[inline]

def Std.Time.ZonedDateTime.toPlainDateTime (dt : ZonedDateTime) : PlainDateTime

Converts a ZonedDateTime to a PlainDateTime

Equations

• dt.toPlainDateTime = dt.date.get

@[inline]

def Std.Time.ZonedDateTime.toDateTime (dt : ZonedDateTime) : DateTime dt.timezone

Converts a ZonedDateTime to a PlainDateTime

Equations

• dt.toDateTime = Std.Time.DateTime.ofTimestamp dt.timestamp dt.timezone

@[inline]

def Std.Time.ZonedDateTime.time (zdt : ZonedDateTime) : PlainTime

Getter for the PlainTime inside of a ZonedDateTime

Equations

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

@[inline]

def Std.Time.ZonedDateTime.year (zdt : ZonedDateTime) : Year.Offset

Getter for the Year inside of a ZonedDateTime

Equations

• zdt.year = zdt.date.get.year

@[inline]

def Std.Time.ZonedDateTime.month (zdt : ZonedDateTime) : Month.Ordinal

Getter for the Month inside of a ZonedDateTime

Equations

• zdt.month = zdt.date.get.month

@[inline]

def Std.Time.ZonedDateTime.day (zdt : ZonedDateTime) : Day.Ordinal

Getter for the Day inside of a ZonedDateTime

Equations

• zdt.day = zdt.date.get.day

@[inline]

def Std.Time.ZonedDateTime.hour (zdt : ZonedDateTime) : Hour.Ordinal

Getter for the Hour inside of a ZonedDateTime

Equations

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

@[inline]

def Std.Time.ZonedDateTime.minute (zdt : ZonedDateTime) : Minute.Ordinal

Getter for the Minute inside of a ZonedDateTime

Equations

• zdt.minute = zdt.date.get.minute

@[inline]

def Std.Time.ZonedDateTime.second (zdt : ZonedDateTime) : Second.Ordinal true

Getter for the Second inside of a ZonedDateTime

Equations

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

@[inline]

def Std.Time.ZonedDateTime.millisecond (dt : ZonedDateTime) : Millisecond.Ordinal

Getter for the Millisecond inside of a ZonedDateTime.

Equations

• dt.millisecond = dt.date.get.time.millisecond

@[inline]

def Std.Time.ZonedDateTime.nanosecond (zdt : ZonedDateTime) : Nanosecond.Ordinal

Getter for the Nanosecond inside of a ZonedDateTime

Equations

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

@[inline]

def Std.Time.ZonedDateTime.offset (zdt : ZonedDateTime) : TimeZone.Offset

Getter for the TimeZone.Offset inside of a ZonedDateTime

Equations

• zdt.offset = zdt.timezone.offset

@[inline]

def Std.Time.ZonedDateTime.weekday (zdt : ZonedDateTime) : Weekday

Returns the weekday.

Equations

• zdt.weekday = zdt.date.get.weekday

@[inline]

def Std.Time.ZonedDateTime.dayOfYear (date : ZonedDateTime) : Day.Ordinal.OfYear date.year.isLeap

Transforms a tuple of a ZonedDateTime into a Day.Ordinal.OfYear.

Equations

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

@[inline]

def Std.Time.ZonedDateTime.weekOfYear (date : ZonedDateTime) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

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

Equations

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

@[inline]

def Std.Time.ZonedDateTime.weekYear (date : ZonedDateTime) (firstDay : Weekday := Weekday.monday) : Year.Offset

Returns the week-based year for the given ZonedDateTime, 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.ZonedDateTime.weekOfMonth (date : ZonedDateTime) : Internal.Bounded.LE 1 5

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

Equations

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

@[inline]

def Std.Time.ZonedDateTime.alignedWeekOfMonth (date : ZonedDateTime) (firstDay : Weekday := Weekday.monday) : Week.Ordinal.OfMonth

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

Equations

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

@[inline]

def Std.Time.ZonedDateTime.quarter (date : ZonedDateTime) : Internal.Bounded.LE 1 4

Determines the quarter of the year for the given ZonedDateTime.

Equations

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

def Std.Time.ZonedDateTime.addDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime

Add Day.Offset to a ZonedDateTime.

Equations

• dt.addDays days = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + days) dt.rules

def Std.Time.ZonedDateTime.subDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime

Subtract Day.Offset from a ZonedDateTime.

Equations

• dt.subDays days = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - days) dt.rules

def Std.Time.ZonedDateTime.addWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime

Add Week.Offset to a ZonedDateTime.

Equations

• dt.addWeeks weeks = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + weeks) dt.rules

def Std.Time.ZonedDateTime.subWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime

Subtract Week.Offset from a ZonedDateTime.

Equations

• dt.subWeeks weeks = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - weeks) dt.rules

def Std.Time.ZonedDateTime.addMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime

Add Month.Offset to a ZonedDateTime, clipping to the last valid day.

Equations

• dt.addMonthsClip months = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.addMonthsClip months) dt.rules

def Std.Time.ZonedDateTime.subMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime

Subtract Month.Offset from a ZonedDateTime, clipping to the last valid day.

Equations

• dt.subMonthsClip months = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.subMonthsClip months) dt.rules

def Std.Time.ZonedDateTime.addMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime

Add Month.Offset to a ZonedDateTime, rolling over excess days.

Equations

• dt.addMonthsRollOver months = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.addMonthsRollOver months) dt.rules

def Std.Time.ZonedDateTime.subMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime

Subtract Month.Offset from a ZonedDateTime, rolling over excess days.

Equations

• dt.subMonthsRollOver months = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.subMonthsRollOver months) dt.rules

def Std.Time.ZonedDateTime.addYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime

Add Year.Offset to a ZonedDateTime, rolling over excess days.

Equations

• dt.addYearsRollOver years = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.addYearsRollOver years) dt.rules

def Std.Time.ZonedDateTime.addYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime

Add Year.Offset to a ZonedDateTime, clipping to the last valid day.

Equations

• dt.addYearsClip years = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.addYearsClip years) dt.rules

def Std.Time.ZonedDateTime.subYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime

Subtract Year.Offset from a ZonedDateTime, clipping to the last valid day.

Equations

• dt.subYearsClip years = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.subYearsClip years) dt.rules

def Std.Time.ZonedDateTime.subYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime

Subtract Year.Offset from a ZonedDateTime, rolling over excess days.

Equations

• dt.subYearsRollOver years = Std.Time.ZonedDateTime.ofPlainDateTime (dt.toPlainDateTime.subYearsRollOver years) dt.rules

def Std.Time.ZonedDateTime.addHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime

Add Hour.Offset to a ZonedDateTime.

Equations

• dt.addHours hours = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + hours) dt.rules

def Std.Time.ZonedDateTime.subHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime

Subtract Hour.Offset from a ZonedDateTime.

Equations

• dt.subHours hours = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - hours) dt.rules

def Std.Time.ZonedDateTime.addMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime

Add Minute.Offset to a ZonedDateTime.

Equations

• dt.addMinutes minutes = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + minutes) dt.rules

def Std.Time.ZonedDateTime.subMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime

Subtract Minute.Offset from a ZonedDateTime.

Equations

• dt.subMinutes minutes = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - minutes) dt.rules

@[inline]

def Std.Time.ZonedDateTime.addMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime

Add Millisecond.Offset to a DateTime.

Equations

• dt.addMilliseconds milliseconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + milliseconds) dt.rules

@[inline]

def Std.Time.ZonedDateTime.subMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime

Subtract Millisecond.Offset from a DateTime.

Equations

• dt.subMilliseconds milliseconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - milliseconds) dt.rules

def Std.Time.ZonedDateTime.addSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime

Add Second.Offset to a ZonedDateTime.

Equations

• dt.addSeconds seconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + seconds) dt.rules

def Std.Time.ZonedDateTime.subSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime

Subtract Second.Offset from a ZonedDateTime.

Equations

• dt.subSeconds seconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - seconds) dt.rules

def Std.Time.ZonedDateTime.addNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime

Add Nanosecond.Offset to a ZonedDateTime.

Equations

• dt.addNanoseconds nanoseconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp + nanoseconds) dt.rules

def Std.Time.ZonedDateTime.subNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime

Subtract Nanosecond.Offset from a ZonedDateTime.

Equations

• dt.subNanoseconds nanoseconds = Std.Time.ZonedDateTime.ofTimestamp (dt.timestamp - nanoseconds) dt.rules

@[inline]

def Std.Time.ZonedDateTime.era (date : ZonedDateTime) : Year.Era

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

Equations

• date.era = date.date.get.era

def Std.Time.ZonedDateTime.withWeekday (dt : ZonedDateTime) (desiredWeekday : Weekday) : ZonedDateTime

Sets the ZonedDateTime to the specified desiredWeekday.

Equations

• dt.withWeekday desiredWeekday = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withWeekday desiredWeekday) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withDaysClip (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withDaysClip days) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withDaysRollOver (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withDaysRollOver days) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withMonthClip (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withMonthClip month) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withMonthRollOver (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withMonthRollOver month) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withYearClip (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withYearClip year) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withYearRollOver (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime

Creates a new ZonedDateTime 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.ZonedDateTime.ofPlainDateTime (dt.date.get.withYearRollOver year) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withHours (dt : ZonedDateTime) (hour : Hour.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime by adjusting the hour component.

Equations

• dt.withHours hour = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withHours hour) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime by adjusting the minute component.

Equations

• dt.withMinutes minute = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withMinutes minute) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime

Creates a new ZonedDateTime by adjusting the second component.

Equations

• dt.withSeconds second = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withSeconds second) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withMilliseconds (dt : ZonedDateTime) (millis : Millisecond.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime by adjusting the nano component with a new millis that will set in the millisecond scale.

Equations

• dt.withMilliseconds millis = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withMilliseconds millis) dt.rules

@[inline]

def Std.Time.ZonedDateTime.withNanoseconds (dt : ZonedDateTime) (nano : Nanosecond.Ordinal) : ZonedDateTime

Creates a new ZonedDateTime by adjusting the nano component.

Equations

• dt.withNanoseconds nano = Std.Time.ZonedDateTime.ofPlainDateTime (dt.date.get.withNanoseconds nano) dt.rules

def Std.Time.ZonedDateTime.inLeapYear (date : ZonedDateTime) : Bool

Checks if the ZonedDateTime is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

def Std.Time.ZonedDateTime.toEpochDay (date : ZonedDateTime) : Day.Offset

Returns the local (civil) date of the ZonedDateTime as a Day.Offset relative to 1970-01-01.

Equations

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

@[inline]

def Std.Time.ZonedDateTime.ofEpochDay (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime

Creates a ZonedDateTime from a local date given as a Day.Offset relative to 1970-01-01, a PlainTime, and ZoneRules. The day offset is interpreted as a local (civil) date, not UTC.

Equations

• Std.Time.ZonedDateTime.ofEpochDay days time zt = Std.Time.ZonedDateTime.ofPlainDateTime (Std.Time.PlainDateTime.ofEpochDay days time) zt

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset : HAdd ZonedDateTime Day.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset : HSub ZonedDateTime Day.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_1 : HAdd ZonedDateTime Week.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_1 : HSub ZonedDateTime Week.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_2 : HAdd ZonedDateTime Hour.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_2 : HSub ZonedDateTime Hour.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_3 : HAdd ZonedDateTime Minute.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_3 : HSub ZonedDateTime Minute.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_4 : HAdd ZonedDateTime Second.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_4 : HSub ZonedDateTime Second.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_5 : HAdd ZonedDateTime Millisecond.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_5 : HSub ZonedDateTime Millisecond.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddOffset_6 : HAdd ZonedDateTime Nanosecond.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubOffset_6 : HSub ZonedDateTime Nanosecond.Offset ZonedDateTime

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHAddDuration : HAdd ZonedDateTime Duration ZonedDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instHSubDuration_1 : HSub ZonedDateTime Duration ZonedDateTime

Equations

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