structure Std.Time.PlainDateTime : Type

Represents a date and time with components for Year, Month, Day, Hour, Minute, Second, and Nanosecond.

• date : PlainDate

  The Date component of a PlainDate

• time : PlainTime

  The Time component of a PlainTime

theorem Std.Time.PlainDateTime.ext_iff {x y : PlainDateTime} : x = y ↔ x.date = y.date ∧ x.time = y.time

theorem Std.Time.PlainDateTime.ext {x y : PlainDateTime} (date : x.date = y.date) (time : x.time = y.time) : x = y

instance Std.Time.instInhabitedPlainDateTime : Inhabited PlainDateTime

instance Std.Time.instDecidableEqPlainDateTime : DecidableEq PlainDateTime

instance Std.Time.instReprPlainDateTime : Repr PlainDateTime

instance Std.Time.instOrdPlainDateTime : Ord PlainDateTime

theorem Std.Time.PlainDateTime.compare_def : compare = compareLex (compareOn fun (x : PlainDateTime) => x.date) (compareOn fun (x : PlainDateTime) => x.time)

instance Std.Time.instTransOrdPlainDateTime : TransOrd PlainDateTime

instance Std.Time.instLawfulEqOrdPlainDateTime : LawfulEqOrd PlainDateTime

def Std.Time.PlainDateTime.toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp

Converts a PlainDateTime to a Timestamp

def Std.Time.PlainDateTime.ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime

Converts a Timestamp to a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset

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

@[inline]

def Std.Time.PlainDateTime.ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime

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

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

Sets the PlainDateTime to the specified desiredWeekday.

@[inline]

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

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

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

Creates a new PlainDateTime by adjusting the month to the given month value, with any out-of-range days clipped to the nearest valid date.

@[inline]

def Std.Time.PlainDateTime.withMonthRollOver (dt : PlainDateTime) (month : Month.Ordinal) : PlainDateTime

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

Creates a new PlainDateTime by adjusting the year to the given year value. The month and day remain unchanged, with any out-of-range days clipped to the nearest valid date.

@[inline]

def Std.Time.PlainDateTime.withYearRollOver (dt : PlainDateTime) (year : Year.Offset) : PlainDateTime

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

Creates a new PlainDateTime by adjusting the hour component of its time to the given value.

@[inline]

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

Creates a new PlainDateTime by adjusting the minute component of its time to the given value.

@[inline]

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

Creates a new PlainDateTime by adjusting the second component of its time to the given value.

@[inline]

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

Creates a new PlainDateTime by adjusting the milliseconds component inside the nano component of its time to the given value.

@[inline]

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

Creates a new PlainDateTime by adjusting the nano component of its time to the given value.

@[inline]

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

Adds a Day.Offset to a PlainDateTime.

@[inline]

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

Subtracts a Day.Offset from a PlainDateTime.

@[inline]

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

Adds a Week.Offset to a PlainDateTime.

@[inline]

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

Subtracts a Week.Offset from a PlainDateTime.

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

Adds a Month.Offset to a PlainDateTime, adjusting the day to the last valid day of the resulting month.

@[inline]

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

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

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

Adds a Month.Offset to a PlainDateTime, rolling over excess days to the following month if needed.

@[inline]

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

Subtracts a Month.Offset from a PlainDateTime, adjusting the day to the last valid day of the resulting month.

@[inline]

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

Adds a Month.Offset to a PlainDateTime, rolling over excess days to the following month if needed.

@[inline]

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

Subtracts a Month.Offset from a PlainDateTime, rolling over excess days to the following month if needed.

@[inline]

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

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

@[inline]

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

Subtracts a Year.Offset from a PlainDateTime, adjusting the day to the last valid day of the resulting month.

@[inline]

def Std.Time.PlainDateTime.addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime

Adds a Nanosecond.Offset to a PlainDateTime, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow.

@[inline]

def Std.Time.PlainDateTime.subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime

Subtracts a Nanosecond.Offset from a PlainDateTime, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.

@[inline]

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

Adds an Hour.Offset to a PlainDateTime, adjusting the date if the hour overflows.

@[inline]

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

Subtracts an Hour.Offset from a PlainDateTime, adjusting the date if the hour underflows.

@[inline]

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

Adds a Minute.Offset to a PlainDateTime, adjusting the hour and date if the minutes overflow.

@[inline]

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

Subtracts a Minute.Offset from a PlainDateTime, adjusting the hour and date if the minutes underflow.

@[inline]

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

Adds a Second.Offset to a PlainDateTime, adjusting the minute, hour, and date if the seconds overflow.

@[inline]

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

Subtracts a Second.Offset from a PlainDateTime, adjusting the minute, hour, and date if the seconds underflow.

@[inline]

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

Adds a Millisecond.Offset to a PlainDateTime, adjusting the second, minute, hour, and date if the milliseconds overflow.

@[inline]

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

Subtracts a Millisecond.Offset from a PlainDateTime, adjusting the second, minute, hour, and date if the milliseconds underflow.

@[inline]

def Std.Time.PlainDateTime.year (dt : PlainDateTime) : Year.Offset

Getter for the Year inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.month (dt : PlainDateTime) : Month.Ordinal

Getter for the Month inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.day (dt : PlainDateTime) : Day.Ordinal

Getter for the Day inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.weekday (dt : PlainDateTime) : Weekday

Getter for the Weekday inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.hour (dt : PlainDateTime) : Hour.Ordinal

Getter for the Hour inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.minute (dt : PlainDateTime) : Minute.Ordinal

Getter for the Minute inside of a PlainDateTime.

@[inline]

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

Getter for the Millisecond inside of a PlainDateTime.

@[inline]

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

Getter for the Second inside of a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.nanosecond (dt : PlainDateTime) : Nanosecond.Ordinal

Getter for the Nanosecond.Ordinal inside of a PlainDateTime.

@[inline]

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

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

@[inline]

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

Checks if the PlainDateTime is in a leap year.

@[inline]

def Std.Time.PlainDateTime.weekOfYear (date : PlainDateTime) : Week.Ordinal

Determines the week of the year for the given PlainDateTime.

def Std.Time.PlainDateTime.weekOfMonth (date : PlainDateTime) : Internal.Bounded.LE 1 5

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

@[inline]

def Std.Time.PlainDateTime.alignedWeekOfMonth (date : PlainDateTime) : Week.Ordinal.OfMonth

Determines the week of the month for the given PlainDateTime. 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.PlainDateTime.dayOfYear (date : PlainDateTime) : Day.Ordinal.OfYear date.year.isLeap

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

@[inline]

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

Determines the quarter of the year for the given PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.atTime : PlainDate → PlainTime → PlainDateTime

Combines a PlainDate and PlainTime into a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.atDate (time : PlainTime) (date : PlainDate) : PlainDateTime

Combines a PlainTime and PlainDate into a PlainDateTime.

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

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

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

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

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

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

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

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

instance Std.Time.PlainDateTime.instHAddOffset_4 : HAdd PlainDateTime Millisecond.Offset PlainDateTime

instance Std.Time.PlainDateTime.instHSubOffset_4 : HSub PlainDateTime Millisecond.Offset PlainDateTime

instance Std.Time.PlainDateTime.instHAddOffset_5 : HAdd PlainDateTime Second.Offset PlainDateTime

instance Std.Time.PlainDateTime.instHSubOffset_5 : HSub PlainDateTime Second.Offset PlainDateTime

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

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

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

@[inline]

def Std.Time.PlainDate.atTime : PlainDate → PlainTime → PlainDateTime

Combines a PlainDate and PlainTime into a PlainDateTime.

@[inline]

def Std.Time.PlainTime.atDate (time : PlainTime) (date : PlainDate) : PlainDateTime

Combines a PlainTime and PlainDate into a PlainDateTime.