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_reducible]

instance Std.Time.instInhabitedPlainDateTime : Inhabited PlainDateTime

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

@[instance_reducible]

instance Std.Time.instDecidableEqPlainDateTime : DecidableEq PlainDateTime

@[instance_reducible]

instance Std.Time.instReprPlainDateTime : Repr PlainDateTime

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

@[instance_reducible]

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.toWallTime (dt : PlainDateTime) : WallTime

Converts a PlainDateTime to a WallTime.

def Std.Time.PlainDateTime.ofWallTime (stamp : WallTime) : PlainDateTime

Converts a WallTime to a PlainDateTime.

@[inline]

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

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

@[inline]

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

Converts the number of days relative to 1970-01-01 as a PlainDateTime.

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

Sets the PlainDateTime to the specified Weekday.

@[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) (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 PlainDateTime, 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.PlainDateTime.weekYear (date : PlainDateTime) (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 PlainDateTime, 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.PlainDateTime.alignedWeekOfMonth (date : PlainDateTime) : Week.Aligned.Ordinal

Returns the aligned week of the month for a PlainDateTime. 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.PlainDateTime.weekOfMonth (date : PlainDateTime) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

Returns the week of the month for the given PlainDateTime, 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.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_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[inline]

def Std.Time.PlainDateTime.ofPlainDate (date : PlainDate) : PlainDateTime

Wraps a PlainDate in a PlainDateTime with midnight as the time component.

@[inline]

def Std.Time.PlainDateTime.toPlainDate (pdt : PlainDateTime) : PlainDate

Extracts the PlainDate component from a PlainDateTime.

@[inline]

def Std.Time.PlainDateTime.toPlainTime (pdt : PlainDateTime) : PlainTime

Extracts the PlainTime component from a PlainDateTime.

@[instance_reducible]

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

@[inline]

def Std.Time.PlainDate.toWallTime (pd : PlainDate) : WallTime

Converts a PlainDate to a WallTime.

@[inline]

def Std.Time.PlainDate.ofWallTime (wt : WallTime) : PlainDate

Converts a WallTime to a PlainDate.

@[instance_reducible]

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

@[inline]

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

Combines a PlainDate and PlainTime into a PlainDateTime.

@[inline]

def Std.Time.PlainTime.toWallTime (pt : PlainTime) : WallTime

Converts a PlainTime to a WallTime.

@[inline]

def Std.Time.PlainTime.ofWallTime (wt : WallTime) : PlainTime

Converts a WallTime to a PlainTime.

@[inline]

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

Combines a PlainTime and PlainDate into a PlainDateTime.