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

@[implicit_reducible]

instance Std.Time.instInhabitedPlainDateTime : Inhabited PlainDateTime

Equations

• Std.Time.instInhabitedPlainDateTime = { default := Std.Time.instInhabitedPlainDateTime.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 ⋯

@[implicit_reducible]

instance Std.Time.instDecidableEqPlainDateTime : DecidableEq PlainDateTime

Equations

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

@[implicit_reducible]

instance Std.Time.instReprPlainDateTime : Repr PlainDateTime

Equations

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

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

Equations

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

@[implicit_reducible]

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

Converts a PlainDateTime to a WallTime.

Equations

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

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

Converts a WallTime to a PlainDateTime.

Equations

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

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

Equations

• pdt.toEpochDay = pdt.date.toEpochDay

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

Equations

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

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

Sets the PlainDateTime to the specified Weekday.

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.ofWallTime (dt.toWallTime + 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) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

Determines the week of the year for the given PlainDateTime, using firstDay as the start of the week.

Equations

• date.weekOfYear firstDay = date.date.weekOfYear firstDay

@[inline]

def Std.Time.PlainDateTime.weekYear (date : PlainDateTime) (firstDay : Weekday := Weekday.monday) : Year.Offset

Returns the week-based year for the given PlainDateTime, 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.weekYear firstDay

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) (firstDay : Weekday := Weekday.monday) : Week.Ordinal.OfMonth

Determines the week of the month for the given PlainDateTime, using firstDay as the start of the week.

Equations

• date.alignedWeekOfMonth firstDay = date.date.alignedWeekOfMonth firstDay

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 }