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.

instance Std.Time.instInhabitedZonedDateTime : Inhabited ZonedDateTime

Equations

• Std.Time.instInhabitedZonedDateTime = { default := { date := { fn := default }, timestamp := default, rules := default, timezone := default } }

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

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.

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 ZoleRules to a new one.

Equations

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

@[inline]

def Std.Time.ZonedDateTime.ofPlainDateTimeAssumingUTC (date : PlainDateTime) (tz : TimeZone.ZoneRules) : ZonedDateTime

Creates a new ZonedDateTime out of a PlainDateTime. It assumes that the PlainDateTime is relative to UTC.

Equations

• Std.Time.ZonedDateTime.ofPlainDateTimeAssumingUTC date tz = Std.Time.ZonedDateTime.ofTimestamp date.toTimestampAssumingUTC 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) : Week.Ordinal

Determines the week of the year for the given ZonedDateTime.

Equations

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

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) : Week.Ordinal.OfMonth

Determines the week of the month for the given ZonedDateTime. The week of the month is calculated based on the day of the month and the weekday. Each week starts on Monday because the entire library is based on the Gregorian Calendar.

Equations

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

@[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.toPlainDateTimeAssumingUTC.addDays days).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subDays days).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addWeeks weeks).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subWeeks weeks).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.addMonthsClip months).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.subMonthsClip months).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.addMonthsRollOver months).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.subMonthsRollOver months).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.addYearsRollOver years).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.addYearsClip years).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.subYearsClip years).toTimestampAssumingUTC 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.ofTimestamp (dt.timestamp.toPlainDateTimeAssumingUTC.subYearsRollOver years).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addHours hours).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subHours hours).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addMinutes minutes).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subMinutes minutes).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addMilliseconds milliseconds).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subMilliseconds milliseconds).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addSeconds seconds).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subSeconds seconds).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.addNanoseconds nanoseconds).toTimestampAssumingUTC 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.toPlainDateTimeAssumingUTC.subNanoseconds nanoseconds).toTimestampAssumingUTC 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.toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset

Converts a ZonedDateTime to the number of days since the UNIX epoch.

Equations

• date.toDaysSinceUNIXEpoch = date.date.get.toDaysSinceUNIXEpoch

@[inline]

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

Converts a ZonedDateTime to the number of days since the UNIX epoch.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 }

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 }

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 }