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 {x y : PlainDateTime} (date : x.date = y.date) (time : x.time = y.time) : x = y

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

instance Std.Time.instInhabitedPlainDateTime : Inhabited PlainDateTime

Equations

• Std.Time.instInhabitedPlainDateTime = { default := Std.Time.instInhabitedPlainDateTime.default }

def Std.Time.instInhabitedPlainDateTime.default : PlainDateTime

Equations

• Std.Time.instInhabitedPlainDateTime.default = { date := default, time := default }

def Std.Time.instDecidableEqPlainDateTime.decEq (x✝ x✝¹ : PlainDateTime) : Decidable (x✝ = x✝¹)

Equations

• Std.Time.instDecidableEqPlainDateTime.decEq { date := a, time := a_1 } { date := b, time := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Std.Time.instDecidableEqPlainDateTime : DecidableEq PlainDateTime

Equations

• Std.Time.instDecidableEqPlainDateTime = Std.Time.instDecidableEqPlainDateTime.decEq

def Std.Time.instReprPlainDateTime.repr : PlainDateTime → Nat → Std.Format

Equations

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

instance Std.Time.instReprPlainDateTime : Repr PlainDateTime

Equations

• Std.Time.instReprPlainDateTime = { reprPrec := Std.Time.instReprPlainDateTime.repr }

instance Std.Time.instOrdPlainDateTime : Ord PlainDateTime

Equations

• Std.Time.instOrdPlainDateTime = { compare := compareLex (compareOn fun (x : Std.Time.PlainDateTime) => x.date) (compareOn fun (x : Std.Time.PlainDateTime) => x.time) }

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

Equations

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

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

Converts a Timestamp to a PlainDateTime.

Equations

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

@[inline]

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

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

Equations

• pdt.toDaysSinceUNIXEpoch = pdt.date.toDaysSinceUNIXEpoch

@[inline]

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

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

Equations

• Std.Time.PlainDateTime.ofDaysSinceUNIXEpoch days time = { date := Std.Time.PlainDate.ofDaysSinceUNIXEpoch days, time := time }

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

Sets the PlainDateTime to the specified desiredWeekday.

Equations

• dt.withWeekday desiredWeekday = { date := dt.date.withWeekday desiredWeekday, time := dt.time }

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

Equations

• dt.withDaysClip days = { date := Std.Time.PlainDate.ofYearMonthDayClip dt.date.year dt.date.month days, time := dt.time }

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

Equations

• dt.withDaysRollOver days = { date := Std.Time.PlainDate.rollOver dt.date.year dt.date.month days, time := dt.time }

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

Equations

• dt.withMonthClip month = { date := Std.Time.PlainDate.ofYearMonthDayClip dt.date.year month dt.date.day, time := dt.time }

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

Equations

• dt.withMonthRollOver month = { date := Std.Time.PlainDate.rollOver dt.date.year month dt.date.day, time := dt.time }

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

Equations

• dt.withYearClip year = { date := Std.Time.PlainDate.ofYearMonthDayClip year dt.date.month dt.date.day, time := dt.time }

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

Equations

• dt.withYearRollOver year = { date := Std.Time.PlainDate.rollOver year dt.date.month dt.date.day, time := dt.time }

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

Equations

• dt.withHours hour = { date := dt.date, time := have __src := dt.time; { hour := hour, minute := __src.minute, second := __src.second, nanosecond := __src.nanosecond } }

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

Equations

• dt.withMinutes minute = { date := dt.date, time := have __src := dt.time; { hour := __src.hour, minute := minute, second := __src.second, nanosecond := __src.nanosecond } }

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

Equations

• dt.withSeconds second = { date := dt.date, time := have __src := dt.time; { hour := __src.hour, minute := __src.minute, second := second, nanosecond := __src.nanosecond } }

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

Equations

• dt.withMilliseconds millis = { date := dt.date, time := dt.time.withMilliseconds millis }

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

Equations

• dt.withNanoseconds nano = { date := dt.date, time := dt.time.withNanoseconds nano }

@[inline]

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

Adds a Day.Offset to a PlainDateTime.

Equations

• dt.addDays days = { date := dt.date.addDays days, time := dt.time }

@[inline]

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

Subtracts a Day.Offset from a PlainDateTime.

Equations

• dt.subDays days = { date := dt.date.subDays days, time := dt.time }

@[inline]

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

Adds a Week.Offset to a PlainDateTime.

Equations

• dt.addWeeks weeks = { date := dt.date.addWeeks weeks, time := dt.time }

@[inline]

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

Subtracts a Week.Offset from a PlainDateTime.

Equations

• dt.subWeeks weeks = { date := dt.date.subWeeks weeks, time := dt.time }

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.

Equations

• dt.addMonthsClip months = { date := dt.date.addMonthsClip months, time := dt.time }

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

Equations

• dt.subMonthsClip months = { date := dt.date.subMonthsClip months, time := dt.time }

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.

Equations

• dt.addMonthsRollOver months = { date := dt.date.addMonthsRollOver months, time := dt.time }

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

Equations

• dt.subMonthsRollOver months = { date := dt.date.subMonthsRollOver months, time := dt.time }

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

Equations

• dt.addYearsRollOver years = { date := dt.date.addYearsRollOver years, time := dt.time }

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

Equations

• dt.addYearsClip years = { date := dt.date.addYearsClip years, time := dt.time }

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

Equations

• dt.subYearsRollOver years = { date := dt.date.subYearsRollOver years, time := dt.time }

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

Equations

• dt.subYearsClip years = { date := dt.date.subYearsClip years, time := dt.time }

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

Equations

• dt.addNanoseconds nanos = Std.Time.PlainDateTime.ofTimestampAssumingUTC (dt.toTimestampAssumingUTC + nanos)

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

Equations

• dt.subNanoseconds nanos = dt.addNanoseconds (-nanos)

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

Equations

• dt.addHours hours = dt.addNanoseconds hours.toNanoseconds

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

Equations

• dt.subHours hours = dt.addHours (-hours)

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

Equations

• dt.addMinutes minutes = dt.addNanoseconds minutes.toNanoseconds

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

Equations

• dt.subMinutes minutes = dt.addMinutes (-minutes)

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

Equations

• dt.addSeconds seconds = dt.addNanoseconds seconds.toNanoseconds

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

Equations

• dt.subSeconds seconds = dt.addSeconds (-seconds)

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

Equations

• dt.addMilliseconds milliseconds = dt.addNanoseconds milliseconds.toNanoseconds

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

Equations

• dt.subMilliseconds milliseconds = dt.addMilliseconds (-milliseconds)

@[inline]

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

Getter for the Year inside of a PlainDateTime.

Equations

• dt.year = dt.date.year

@[inline]

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

Getter for the Month inside of a PlainDateTime.

Equations

• dt.month = dt.date.month

@[inline]

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

Getter for the Day inside of a PlainDateTime.

Equations

• dt.day = dt.date.day

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

Equations

• dt.hour = dt.time.hour

@[inline]

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

Getter for the Minute inside of a PlainDateTime.

Equations

• dt.minute = dt.time.minute

@[inline]

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

Getter for the Millisecond inside of a PlainDateTime.

Equations

• dt.millisecond = dt.time.millisecond

@[inline]

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

Getter for the Second inside of a PlainDateTime.

Equations

• dt.second = dt.time.second

@[inline]

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

Getter for the Nanosecond.Ordinal inside of a PlainDateTime.

Equations

• dt.nanosecond = dt.time.nanosecond

@[inline]

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

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

Equations

• date.era = date.date.era

@[inline]

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

Checks if the PlainDateTime is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

@[inline]

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

Determines the week of the year for the given PlainDateTime.

Equations

• date.weekOfYear = date.date.weekOfYear

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

Equations

• date.weekOfMonth = date.date.weekOfMonth

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

Equations

• date.alignedWeekOfMonth = date.date.alignedWeekOfMonth

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

Equations

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

@[inline]

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

Determines the quarter of the year for the given PlainDateTime.

Equations

• date.quarter = date.date.quarter

@[inline]

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

Combines a PlainDate and PlainTime into a PlainDateTime.

Equations

• Std.Time.PlainDateTime.atTime = Std.Time.PlainDateTime.mk

@[inline]

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

Combines a PlainTime and PlainDate into a PlainDateTime.

Equations

• Std.Time.PlainDateTime.atDate time date = { date := date, time := time }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Std.Time.PlainDateTime.instHAddOffset_4 = { hAdd := Std.Time.PlainDateTime.addMilliseconds }

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

Equations

• Std.Time.PlainDateTime.instHSubOffset_4 = { hSub := Std.Time.PlainDateTime.addMilliseconds }

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

Equations

• Std.Time.PlainDateTime.instHAddOffset_5 = { hAdd := Std.Time.PlainDateTime.addSeconds }

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

Equations

• Std.Time.PlainDateTime.instHSubOffset_5 = { hSub := Std.Time.PlainDateTime.subSeconds }

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Combines a PlainDate and PlainTime into a PlainDateTime.

Equations

• Std.Time.PlainDate.atTime = Std.Time.PlainDateTime.mk

@[inline]

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

Combines a PlainTime and PlainDate into a PlainDateTime.

Equations

• time.atDate date = { date := date, time := time }