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

@[inline]

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

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

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

@[inline]

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

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

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

@[inline]

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

Creates a new Timestamp out of a ZonedDateTime.

@[inline]

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

Changes the ZoneRules to a new one.

@[inline]

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

Converts a ZonedDateTime to a PlainDateTime

@[inline]

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

Converts a ZonedDateTime to a PlainDateTime

@[inline]

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

Getter for the PlainTime inside of a ZonedDateTime

@[inline]

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

Getter for the Year inside of a ZonedDateTime

@[inline]

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

Getter for the Month inside of a ZonedDateTime

@[inline]

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

Getter for the Day inside of a ZonedDateTime

@[inline]

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

Getter for the Hour inside of a ZonedDateTime

@[inline]

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

Getter for the Minute inside of a ZonedDateTime

@[inline]

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

Getter for the Second inside of a ZonedDateTime

@[inline]

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

Getter for the Millisecond inside of a ZonedDateTime.

@[inline]

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

Getter for the Nanosecond inside of a ZonedDateTime

@[inline]

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

Getter for the TimeZone.Offset inside of a ZonedDateTime

@[inline]

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

Returns the 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.

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

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

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).

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

@[inline]

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

Determines the quarter of the year for the given ZonedDateTime.

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

Add Day.Offset to a ZonedDateTime.

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

Subtract Day.Offset from a ZonedDateTime.

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

Add Week.Offset to a ZonedDateTime.

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

Subtract Week.Offset from a ZonedDateTime.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Add Hour.Offset to a ZonedDateTime.

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

Subtract Hour.Offset from a ZonedDateTime.

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

Add Minute.Offset to a ZonedDateTime.

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

Subtract Minute.Offset from a ZonedDateTime.

@[inline]

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

Add Millisecond.Offset to a DateTime.

@[inline]

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

Subtract Millisecond.Offset from a DateTime.

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

Add Second.Offset to a ZonedDateTime.

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

Subtract Second.Offset from a ZonedDateTime.

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

Add Nanosecond.Offset to a ZonedDateTime.

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

Subtract Nanosecond.Offset from a ZonedDateTime.

@[inline]

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

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

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

Sets the ZonedDateTime to the specified desiredWeekday.

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

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

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

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

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

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

@[inline]

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

Creates a new ZonedDateTime by adjusting the hour component.

@[inline]

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

Creates a new ZonedDateTime by adjusting the minute component.

@[inline]

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

Creates a new ZonedDateTime by adjusting the second component.

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

@[inline]

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

Creates a new ZonedDateTime by adjusting the nano component.

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

Checks if the ZonedDateTime is in a leap year.

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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