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.

@[implicit_reducible]

instance Std.Time.instInhabitedDateTime : Inhabited DateTime

Equations

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

@[inline]

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

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

Equations

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

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

Equations

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

@[inline]

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

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

Equations

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

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

Equations

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

@[inline]

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

Creates a new Timestamp out of a DateTime.

Equations

• date.toTimestamp = date.timestamp

@[inline]

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

Changes the ZoneRules to a new one.

Equations

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

@[inline]

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

Converts a DateTime to a PlainDateTime

Equations

• dt.toPlainDateTime = dt.date.get

@[inline]

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

Getter for the PlainTime inside of a DateTime

Equations

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

@[inline]

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

Getter for the Year inside of a DateTime

Equations

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

@[inline]

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

Getter for the Month inside of a DateTime

Equations

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

@[inline]

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

Getter for the Day inside of a DateTime

Equations

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

@[inline]

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

Getter for the Hour inside of a DateTime

Equations

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

@[inline]

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

Getter for the Minute inside of a DateTime

Equations

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

@[inline]

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

Getter for the Second inside of a DateTime

Equations

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

@[inline]

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

Getter for the Millisecond inside of a DateTime.

Equations

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

@[inline]

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

Getter for the Nanosecond inside of a DateTime

Equations

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

@[inline]

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

Getter for the TimeZone.Offset inside of a DateTime

Equations

• zdt.offset = zdt.timezone.offset

@[inline]

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

Returns the weekday.

Equations

• zdt.weekday = zdt.date.get.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.

Equations

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

@[inline]

def Std.Time.DateTime.weekOfYear (date : DateTime) (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 (date : DateTime) (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 (date : DateTime) : 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 (date : DateTime) (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 (date : DateTime) : Internal.Bounded.LE 1 4

Determines the quarter of the year for the given DateTime.

Equations

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

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

Add Day.Offset to a DateTime.

Equations

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

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

Subtract Day.Offset from a DateTime.

Equations

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

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

Add Week.Offset to a DateTime.

Equations

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

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

Subtract Week.Offset from a DateTime.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Add Hour.Offset to a DateTime.

Equations

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

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

Subtract Hour.Offset from a DateTime.

Equations

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

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

Add Minute.Offset to a DateTime.

Equations

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

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

Subtract Minute.Offset from a DateTime.

Equations

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

@[inline]

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

Add Millisecond.Offset to a DateTime.

Equations

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

@[inline]

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

Subtract Millisecond.Offset from a DateTime.

Equations

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

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

Add Second.Offset to a DateTime.

Equations

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

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

Subtract Second.Offset from a DateTime.

Equations

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

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

Add Nanosecond.Offset to a DateTime.

Equations

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

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

Subtract Nanosecond.Offset from a DateTime.

Equations

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

@[inline]

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

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

Equations

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

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

Sets the DateTime to the specified desiredWeekday.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Creates a new DateTime by adjusting the hour component.

Equations

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

@[inline]

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

Creates a new DateTime by adjusting the minute component.

Equations

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

@[inline]

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

Creates a new DateTime by adjusting the second component.

Equations

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

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

Equations

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

@[inline]

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

Creates a new DateTime by adjusting the nano component.

Equations

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

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

Checks if the DateTime is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

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.

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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