source
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`

Instances For

source
theorem Std.Time.PlainDateTime.ext {x y : PlainDateTime} (date : x.date = y.date) (time : x.time = y.time) :
x = y
source
theorem Std.Time.PlainDateTime.ext_iff {x y : PlainDateTime} :
x = y ↔ x.date = y.date ∧ x.time = y.time
source
instance Std.Time.instInhabitedPlainDateTime :
Inhabited PlainDateTime
Equations

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

source
def Std.Time.instInhabitedPlainDateTime.default :
PlainDateTime
Equations

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

Instances For

source
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 ⋯

Instances For

source
instance Std.Time.instDecidableEqPlainDateTime :
DecidableEq PlainDateTime
Equations

- Std.Time.instDecidableEqPlainDateTime = Std.Time.instDecidableEqPlainDateTime.decEq

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

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

Instances For

source
instance Std.Time.instReprPlainDateTime :
Repr PlainDateTime
Equations

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

source
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) }

source
theorem Std.Time.PlainDateTime.compare_def :
compare = compareLex (compareOn fun (x : PlainDateTime) => x.date) (compareOn fun (x : PlainDateTime) => x.time)
source
instance Std.Time.instTransOrdPlainDateTime :
TransOrd PlainDateTime
source
instance Std.Time.instLawfulEqOrdPlainDateTime :
LawfulEqOrd PlainDateTime
source
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.

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 }

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 }

Instances For

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

Instances For

source
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 }

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

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

Instances For

source
@[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)

Instances For

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

Instances For

source
@[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)

Instances For

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

Instances For

source
@[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)

Instances For

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

Instances For

source
@[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)

Instances For

source
@[inline]
def Std.Time.PlainDateTime.year (dt : PlainDateTime) :
Year.Offset

Getter for the `Year` inside of a `PlainDateTime`.

Equations

- dt.year = dt.date.year

Instances For

source
@[inline]
def Std.Time.PlainDateTime.month (dt : PlainDateTime) :
Month.Ordinal

Getter for the `Month` inside of a `PlainDateTime`.

Equations

- dt.month = dt.date.month

Instances For

source
@[inline]
def Std.Time.PlainDateTime.day (dt : PlainDateTime) :
Day.Ordinal

Getter for the `Day` inside of a `PlainDateTime`.

Equations

- dt.day = dt.date.day

Instances For

source
@[inline]
def Std.Time.PlainDateTime.weekday (dt : PlainDateTime) :
Weekday

Getter for the `Weekday` inside of a `PlainDateTime`.

Instances For

source
@[inline]
def Std.Time.PlainDateTime.hour (dt : PlainDateTime) :
Hour.Ordinal

Getter for the `Hour` inside of a `PlainDateTime`.

Equations

- dt.hour = dt.time.hour

Instances For

source
@[inline]
def Std.Time.PlainDateTime.minute (dt : PlainDateTime) :
Minute.Ordinal

Getter for the `Minute` inside of a `PlainDateTime`.

Equations

- dt.minute = dt.time.minute

Instances For

source
@[inline]
def Std.Time.PlainDateTime.millisecond (dt : PlainDateTime) :
Millisecond.Ordinal

Getter for the `Millisecond` inside of a `PlainDateTime`.

Equations

- dt.millisecond = dt.time.millisecond

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[inline]
def Std.Time.PlainDateTime.inLeapYear (date : PlainDateTime) :
Bool

Checks if the `PlainDateTime` is in a leap year.

Equations

- date.inLeapYear = date.year.isLeap

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
@[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), ⋯⟩

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
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 }

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

Instances For

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

Instances For