structure Std.Time.DateTime (tz : TimeZone) : Type

Represents a specific point in time associated with a TimeZone.

• timestamp : Timestamp

  Timestamp represents the exact moment in time. It's a UTC related Timestamp.

• date : Thunk PlainDateTime

  Date is a Thunk containing the PlainDateTime that represents the local date and time, it's used for accessing data like day and month without having to recompute the data every time.

@[implicit_reducible]

instance Std.Time.instBEqDateTime {tz : TimeZone} : BEq (DateTime tz)

@[implicit_reducible]

instance Std.Time.instOrdDateTime {tz : TimeZone} : Ord (DateTime tz)

instance Std.Time.instTransOrdDateTime {tz : TimeZone} : TransOrd (DateTime tz)

instance Std.Time.instLawfulBEqOrdDateTime {tz : TimeZone} : LawfulBEqOrd (DateTime tz)

@[inline]

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

Creates a new DateTime out of a Timestamp that is in a TimeZone.

@[implicit_reducible]

instance Std.Time.DateTime.instInhabited {tz : TimeZone} : Inhabited (DateTime tz)

def Std.Time.DateTime.toDaysSinceUNIXEpoch {tz : TimeZone} (date : DateTime tz) : Day.Offset

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

@[inline]

def Std.Time.DateTime.toTimestamp {tz : TimeZone} (date : DateTime tz) : Timestamp

Creates a Timestamp out of a DateTime.

@[inline]

def Std.Time.DateTime.convertTimeZone {tz : TimeZone} (date : DateTime tz) (tz₁ : TimeZone) : DateTime tz₁

Changes the TimeZone to a new one.

@[inline]

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

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

@[inline]

def Std.Time.DateTime.ofPlainDateTime (date : PlainDateTime) (tz : TimeZone) : DateTime tz

Creates a new DateTime from a PlainDateTime, assuming that the PlainDateTime is relative to the given TimeZone.

@[inline]

def Std.Time.DateTime.addHours {tz : TimeZone} (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz

Add Hour.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subHours {tz : TimeZone} (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz

Subtract Hour.Offset from a DateTime.

@[inline]

def Std.Time.DateTime.addMinutes {tz : TimeZone} (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz

Add Minute.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subMinutes {tz : TimeZone} (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz

Subtract Minute.Offset from a DateTime.

@[inline]

def Std.Time.DateTime.addSeconds {tz : TimeZone} (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz

Add Second.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subSeconds {tz : TimeZone} (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz

Subtract Second.Offset from a DateTime.

@[inline]

def Std.Time.DateTime.addMilliseconds {tz : TimeZone} (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz

Add Millisecond.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subMilliseconds {tz : TimeZone} (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz

Subtract Millisecond.Offset from a DateTime.

@[inline]

def Std.Time.DateTime.addNanoseconds {tz : TimeZone} (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz

Add Nanosecond.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subNanoseconds {tz : TimeZone} (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz

Subtract Nanosecond.Offset from a DateTime.

@[inline]

def Std.Time.DateTime.addDays {tz : TimeZone} (dt : DateTime tz) (days : Day.Offset) : DateTime tz

Add Day.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subDays {tz : TimeZone} (dt : DateTime tz) (days : Day.Offset) : DateTime tz

Subtracts Day.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.addWeeks {tz : TimeZone} (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz

Add Week.Offset to a DateTime.

@[inline]

def Std.Time.DateTime.subWeeks {tz : TimeZone} (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz

Subtracts Week.Offset to a DateTime.

def Std.Time.DateTime.addMonthsClip {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Add Month.Offset to a DateTime, it clips the day to the last valid day of that month.

@[inline]

def Std.Time.DateTime.subMonthsClip {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Subtracts Month.Offset from a DateTime, it clips the day to the last valid day of that month.

def Std.Time.DateTime.addMonthsRollOver {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Add Month.Offset from a DateTime, this function rolls over any excess days into the following month.

@[inline]

def Std.Time.DateTime.subMonthsRollOver {tz : TimeZone} (dt : DateTime tz) (months : Month.Offset) : DateTime tz

Subtract Month.Offset from a DateTime, this function rolls over any excess days into the following month.

@[inline]

def Std.Time.DateTime.addYearsRollOver {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Add Year.Offset to a DateTime, this function rolls over any excess days into the following month.

@[inline]

def Std.Time.DateTime.addYearsClip {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Add Year.Offset to a DateTime, it clips the day to the last valid day of that month.

@[inline]

def Std.Time.DateTime.subYearsRollOver {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Subtract Year.Offset from a DateTime, this function rolls over any excess days into the following month.

@[inline]

def Std.Time.DateTime.subYearsClip {tz : TimeZone} (dt : DateTime tz) (years : Year.Offset) : DateTime tz

Subtract Year.Offset from to a DateTime, it clips the day to the last valid day of that month.

@[inline]

def Std.Time.DateTime.withDaysClip {tz : TimeZone} (dt : DateTime tz) (days : Day.Ordinal) : DateTime tz

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

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

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

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

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

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

Creates a new DateTime tz by adjusting the hour component.

@[inline]

def Std.Time.DateTime.withMinutes {tz : TimeZone} (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the minute component.

@[inline]

def Std.Time.DateTime.withSeconds {tz : TimeZone} (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz

Creates a new DateTime tz by adjusting the second component.

@[inline]

def Std.Time.DateTime.withNanoseconds {tz : TimeZone} (dt : DateTime tz) (nano : Nanosecond.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the nano component.

@[inline]

def Std.Time.DateTime.withMilliseconds {tz : TimeZone} (dt : DateTime tz) (milli : Millisecond.Ordinal) : DateTime tz

Creates a new DateTime tz by adjusting the millisecond component.

@[inline]

def Std.Time.DateTime.toPlainDateTime {tz : TimeZone} (dt : DateTime tz) : PlainDateTime

Converts a Timestamp to a PlainDateTime

@[inline]

def Std.Time.DateTime.year {tz : TimeZone} (dt : DateTime tz) : Year.Offset

Getter for the Year inside of a DateTime

@[inline]

def Std.Time.DateTime.month {tz : TimeZone} (dt : DateTime tz) : Month.Ordinal

Getter for the Month inside of a DateTime

@[inline]

def Std.Time.DateTime.day {tz : TimeZone} (dt : DateTime tz) : Day.Ordinal

Getter for the Day inside of a DateTime

@[inline]

def Std.Time.DateTime.hour {tz : TimeZone} (dt : DateTime tz) : Hour.Ordinal

Getter for the Hour inside of a DateTime

@[inline]

def Std.Time.DateTime.minute {tz : TimeZone} (dt : DateTime tz) : Minute.Ordinal

Getter for the Minute inside of a DateTime

@[inline]

def Std.Time.DateTime.second {tz : TimeZone} (dt : DateTime tz) : Second.Ordinal true

Getter for the Second inside of a DateTime

@[inline]

def Std.Time.DateTime.millisecond {tz : TimeZone} (dt : DateTime tz) : Millisecond.Ordinal

Getter for the Milliseconds inside of a DateTime

@[inline]

def Std.Time.DateTime.nanosecond {tz : TimeZone} (dt : DateTime tz) : Nanosecond.Ordinal

Getter for the Nanosecond inside of a DateTime

@[inline]

def Std.Time.DateTime.weekday {tz : TimeZone} (dt : DateTime tz) : Weekday

Gets the Weekday of a DateTime.

def Std.Time.DateTime.era {tz : TimeZone} (date : DateTime tz) : Year.Era

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

def Std.Time.DateTime.withWeekday {tz : TimeZone} (dt : DateTime tz) (desiredWeekday : Weekday) : DateTime tz

Sets the DateTime to the specified desiredWeekday.

def Std.Time.DateTime.inLeapYear {tz : TimeZone} (date : DateTime tz) : Bool

Checks if the DateTime is in a leap year.

def Std.Time.DateTime.dayOfYear {tz : TimeZone} (date : DateTime tz) : Day.Ordinal.OfYear date.year.isLeap

Determines the ordinal day of the year for the given DateTime.

@[inline]

def Std.Time.DateTime.weekOfYear {tz : TimeZone} (date : DateTime tz) : Week.Ordinal

Determines the week of the year for the given DateTime.

def Std.Time.DateTime.weekOfMonth {tz : TimeZone} (date : DateTime tz) : Internal.Bounded.LE 1 5

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

@[inline]

def Std.Time.DateTime.alignedWeekOfMonth {tz : TimeZone} (date : DateTime tz) : Week.Ordinal.OfMonth

Determines the week of the month for the given DateTime. 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.

@[inline]

def Std.Time.DateTime.quarter {tz : TimeZone} (date : DateTime tz) : Internal.Bounded.LE 1 4

Determines the quarter of the year for the given DateTime.

@[inline]

def Std.Time.DateTime.time {tz : TimeZone} (zdt : DateTime tz) : PlainTime

Getter for the PlainTime inside of a DateTime

@[inline]

def Std.Time.DateTime.ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz

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

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset {tz : TimeZone} : HAdd (DateTime tz) Day.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset {tz : TimeZone} : HSub (DateTime tz) Day.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_1 {tz : TimeZone} : HAdd (DateTime tz) Week.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_1 {tz : TimeZone} : HSub (DateTime tz) Week.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_2 {tz : TimeZone} : HAdd (DateTime tz) Hour.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_2 {tz : TimeZone} : HSub (DateTime tz) Hour.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_3 {tz : TimeZone} : HAdd (DateTime tz) Minute.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_3 {tz : TimeZone} : HSub (DateTime tz) Minute.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_4 {tz : TimeZone} : HAdd (DateTime tz) Second.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_4 {tz : TimeZone} : HSub (DateTime tz) Second.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_5 {tz : TimeZone} : HAdd (DateTime tz) Millisecond.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_5 {tz : TimeZone} : HSub (DateTime tz) Millisecond.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHAddOffset_6 {tz : TimeZone} : HAdd (DateTime tz) Nanosecond.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubOffset_6 {tz : TimeZone} : HSub (DateTime tz) Nanosecond.Offset (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubDuration {tz tz₁ : TimeZone} : HSub (DateTime tz) (DateTime tz₁) Duration

@[implicit_reducible]

instance Std.Time.DateTime.instHAddDuration {tz : TimeZone} : HAdd (DateTime tz) Duration (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instHSubDuration_1 {tz : TimeZone} : HSub (DateTime tz) Duration (DateTime tz)