structure Std.Time.PlainDateTime : Type

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

• date : Std.Time.PlainDate

  The Date component of a PlainDate

• time : Std.Time.PlainTime

  The Time component of a PlainTime

instance Std.Time.instInhabitedPlainDateTime : Inhabited Std.Time.PlainDateTime

Equations

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

instance Std.Time.instBEqPlainDateTime : BEq Std.Time.PlainDateTime

Equations

• Std.Time.instBEqPlainDateTime = { beq := Std.Time.beqPlainDateTime✝ }

instance Std.Time.instReprPlainDateTime : Repr Std.Time.PlainDateTime

Equations

• Std.Time.instReprPlainDateTime = { reprPrec := Std.Time.reprPlainDateTime✝ }

def Std.Time.PlainDateTime.toTimestampAssumingUTC (dt : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.Timestamp) : Std.Time.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 : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.Day.Offset) (time : Std.Time.PlainTime) : Std.Time.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 : Std.Time.PlainDateTime) (desiredWeekday : Std.Time.Weekday) : Std.Time.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 : Std.Time.PlainDateTime) (days : Std.Time.Day.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (days : Std.Time.Day.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (month : Std.Time.Month.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (month : Std.Time.Month.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (year : Std.Time.Year.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (year : Std.Time.Year.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (hour : Std.Time.Hour.Ordinal) : Std.Time.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 := let __src := dt.time; { hour := hour, minute := __src.minute, second := __src.second, nanosecond := __src.nanosecond } }

@[inline]

def Std.Time.PlainDateTime.withMinutes (dt : Std.Time.PlainDateTime) (minute : Std.Time.Minute.Ordinal) : Std.Time.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 := let __src := dt.time; { hour := __src.hour, minute := minute, second := __src.second, nanosecond := __src.nanosecond } }

@[inline]

def Std.Time.PlainDateTime.withSeconds (dt : Std.Time.PlainDateTime) (second : Sigma Std.Time.Second.Ordinal) : Std.Time.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 := let __src := dt.time; { hour := __src.hour, minute := __src.minute, second := second, nanosecond := __src.nanosecond } }

@[inline]

def Std.Time.PlainDateTime.withMilliseconds (dt : Std.Time.PlainDateTime) (millis : Std.Time.Millisecond.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (nano : Std.Time.Nanosecond.Ordinal) : Std.Time.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 : Std.Time.PlainDateTime) (days : Std.Time.Day.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (days : Std.Time.Day.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (weeks : Std.Time.Week.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (weeks : Std.Time.Week.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (months : Std.Time.Month.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (months : Std.Time.Month.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (months : Std.Time.Month.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (months : Std.Time.Month.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (years : Std.Time.Year.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (years : Std.Time.Year.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (years : Std.Time.Year.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (years : Std.Time.Year.Offset) : Std.Time.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.addHours (dt : Std.Time.PlainDateTime) (hours : Std.Time.Hour.Offset) : Std.Time.PlainDateTime

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

Equations

• dt.addHours hours = { date := dt.date.addDays (Std.Time.Internal.UnitVal.ediv (dt.time.toSeconds + hours.toSeconds) 86400), time := dt.time.addSeconds hours.toSeconds }

@[inline]

def Std.Time.PlainDateTime.subHours (dt : Std.Time.PlainDateTime) (hours : Std.Time.Hour.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (minutes : Std.Time.Minute.Offset) : Std.Time.PlainDateTime

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

Equations

• dt.addMinutes minutes = { date := dt.date.addDays (Std.Time.Internal.UnitVal.ediv (dt.time.toSeconds + minutes.toSeconds) 86400), time := dt.time.addSeconds minutes.toSeconds }

@[inline]

def Std.Time.PlainDateTime.subMinutes (dt : Std.Time.PlainDateTime) (minutes : Std.Time.Minute.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (seconds : Std.Time.Second.Offset) : Std.Time.PlainDateTime

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

Equations

• dt.addSeconds seconds = { date := dt.date.addDays (Std.Time.Internal.UnitVal.ediv (dt.time.toSeconds + seconds) 86400), time := dt.time.addSeconds seconds }

@[inline]

def Std.Time.PlainDateTime.subSeconds (dt : Std.Time.PlainDateTime) (seconds : Std.Time.Second.Offset) : Std.Time.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 : Std.Time.PlainDateTime) (milliseconds : Std.Time.Millisecond.Offset) : Std.Time.PlainDateTime

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

Equations

• dt.addMilliseconds milliseconds = { date := dt.date.addDays (Std.Time.Internal.UnitVal.ediv (dt.time.toMilliseconds + milliseconds) 86400000), time := dt.time.addMilliseconds milliseconds }

@[inline]

def Std.Time.PlainDateTime.subMilliseconds (dt : Std.Time.PlainDateTime) (milliseconds : Std.Time.Millisecond.Offset) : Std.Time.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.addNanoseconds (dt : Std.Time.PlainDateTime) (nanos : Std.Time.Nanosecond.Offset) : Std.Time.PlainDateTime

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

Equations

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

@[inline]

def Std.Time.PlainDateTime.subNanoseconds (dt : Std.Time.PlainDateTime) (nanos : Std.Time.Nanosecond.Offset) : Std.Time.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.year (dt : Std.Time.PlainDateTime) : Std.Time.Year.Offset

Getter for the Year inside of a PlainDateTime.

Equations

• dt.year = dt.date.year

@[inline]

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

Getter for the Month inside of a PlainDateTime.

Equations

• dt.month = dt.date.month

@[inline]

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

Getter for the Day inside of a PlainDateTime.

Equations

• dt.day = dt.date.day

@[inline]

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

Getter for the Weekday inside of a PlainDateTime.

Equations

• dt.weekday = dt.date.weekday

@[inline]

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

Getter for the Hour inside of a PlainDateTime.

Equations

• dt.hour = dt.time.hour

@[inline]

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

Getter for the Minute inside of a PlainDateTime.

Equations

• dt.minute = dt.time.minute

@[inline]

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

Getter for the Millisecond inside of a PlainDateTime.

Equations

• dt.millisecond = dt.time.millisecond

@[inline]

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

Getter for the Second inside of a PlainDateTime.

Equations

• dt.second = dt.time.second.snd

@[inline]

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

Getter for the Nanosecond.Ordinal inside of a PlainDateTime.

Equations

• dt.nanosecond = dt.time.nanosecond

@[inline]

def Std.Time.PlainDateTime.era (date : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.PlainDateTime) : Bool

Checks if the PlainDateTime is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

@[inline]

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

Determines the week of the year for the given PlainDateTime.

Equations

• date.weekOfYear = date.date.weekOfYear

def Std.Time.PlainDateTime.weekOfMonth (date : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.PlainDateTime) : Std.Time.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 : Std.Time.PlainDate → Std.Time.PlainTime → Std.Time.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 : Std.Time.PlainTime) (date : Std.Time.PlainDate) : Std.Time.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 Std.Time.PlainDateTime Std.Time.Day.Offset Std.Time.PlainDateTime

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Std.Time.PlainDateTime.instHAddDuration : HAdd Std.Time.PlainDateTime Std.Time.Duration Std.Time.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 : Std.Time.PlainDate → Std.Time.PlainTime → Std.Time.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 : Std.Time.PlainTime) (date : Std.Time.PlainDate) : Std.Time.PlainDateTime

Combines a PlainTime and PlainDate into a PlainDateTime.

Equations

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