structure Std.Time.DateTime : 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_reducible]

instance Std.Time.instInhabitedDateTime : Inhabited DateTime

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

Creates a new Timestamp out of a DateTime.

@[inline]

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

Changes the ZoneRules to a new one.

@[inline]

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

Converts a DateTime to a PlainDateTime

@[inline]

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

Getter for the PlainTime inside of a DateTime

@[inline]

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

Getter for the Year inside of a DateTime

@[inline]

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

Getter for the Month inside of a DateTime

@[inline]

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

Getter for the Day inside of a DateTime

@[inline]

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

Getter for the Hour inside of a DateTime

@[inline]

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

Getter for the Minute inside of a DateTime

@[inline]

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

Getter for the Second inside of a DateTime

@[inline]

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

Getter for the Millisecond inside of a DateTime.

@[inline]

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

Getter for the Nanosecond inside of a DateTime

@[inline]

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

Getter for the TimeZone.Offset inside of a DateTime

@[inline]

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

Returns the weekday.

@[inline]

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

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

@[inline]

def Std.Time.DateTime.weekOfYear (dt : DateTime) (firstDay : Weekday := Weekday.monday) (minDays : Internal.Bounded.LE 0 6 := Internal.Bounded.LE.mk 4 weekOfYear._proof_1) : Week.OfYear.Ordinal

Determines the week of the year for the given DateTime, using firstDay as the start of the week and minDays as the minimum number of days a week must have in the new year to count as week 1.

@[inline]

def Std.Time.DateTime.weekYear (date : DateTime) (firstDay : Weekday := Weekday.monday) (minDays : Internal.Bounded.LE 0 6 := Internal.Bounded.LE.mk 4 weekOfYear._proof_1) : Year.Offset

Returns the week-based year for the given DateTime, using firstDay as the start of the week and minDays as the minimum number of days a week must have in the new year to count as week 1. The week-based year may differ from the calendar year for dates near the start or end of the year.

def Std.Time.DateTime.alignedWeekOfMonth (date : DateTime) : Week.Aligned.Ordinal

Returns the aligned week of the month for a DateTime. Weeks are fixed 7-day slots starting from day 1: days 1–7 are week 1, days 8–14 are week 2, etc.

@[inline]

def Std.Time.DateTime.weekOfMonth (date : DateTime) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

Returns the week of the month for the given DateTime, where weeks start on firstDay. The first partial week containing day 1 is week 1, so weeks may span fewer than 7 days.

@[inline]

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

Determines the quarter of the year for the given DateTime.

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

Add Day.Offset to a DateTime.

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

Subtract Day.Offset from a DateTime.

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

Add Week.Offset to a DateTime.

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

Subtract Week.Offset from a DateTime.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Add Hour.Offset to a DateTime.

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

Subtract Hour.Offset from a DateTime.

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

Add Minute.Offset to a DateTime.

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

Subtract Minute.Offset from a DateTime.

@[inline]

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

Add Millisecond.Offset to a DateTime.

@[inline]

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

Subtract Millisecond.Offset from a DateTime.

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

Add Second.Offset to a DateTime.

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

Subtract Second.Offset from a DateTime.

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

Add Nanosecond.Offset to a DateTime.

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

Subtract Nanosecond.Offset from a DateTime.

@[inline]

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

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

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

Sets the DateTime to the specified desiredWeekday.

@[inline]

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

Creates a new DateTime 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.DateTime.withDaysRollOver (dt : DateTime) (days : Day.Ordinal) : DateTime

Creates a new DateTime 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.DateTime.withMonthClip (dt : DateTime) (month : Month.Ordinal) : DateTime

Creates a new DateTime 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.DateTime.withMonthRollOver (dt : DateTime) (month : Month.Ordinal) : DateTime

Creates a new DateTime 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.DateTime.withYearClip (dt : DateTime) (year : Year.Offset) : DateTime

Creates a new DateTime 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.DateTime.withYearRollOver (dt : DateTime) (year : Year.Offset) : DateTime

Creates a new DateTime 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.DateTime.withHours (dt : DateTime) (hour : Hour.Ordinal) : DateTime

Creates a new DateTime by adjusting the hour component.

@[inline]

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

Creates a new DateTime by adjusting the minute component.

@[inline]

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

Creates a new DateTime by adjusting the second component.

@[inline]

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

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

@[inline]

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

Creates a new DateTime by adjusting the nano component.

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

Checks if the DateTime is in a leap year.

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

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

@[inline]

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

Creates a DateTime 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.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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