structure Std.Time.PlainTime : Type

Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds.

• hour : Hour.Ordinal

  Hour component of the PlainTime

• minute : Minute.Ordinal

  Minute component of the PlainTime

• second : Second.Ordinal true

  Second component of the PlainTime

• nanosecond : Nanosecond.Ordinal

  Nanoseconds component of the PlainTime

theorem Std.Time.PlainTime.ext_iff {x y : PlainTime} : x = y ↔ x.hour = y.hour ∧ x.minute = y.minute ∧ x.second = y.second ∧ x.nanosecond = y.nanosecond

theorem Std.Time.PlainTime.ext {x y : PlainTime} (hour : x.hour = y.hour) (minute : x.minute = y.minute) (second : x.second = y.second) (nanosecond : x.nanosecond = y.nanosecond) : x = y

def Std.Time.instReprPlainTime.repr : PlainTime → Nat → Std.Format

Equations

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

instance Std.Time.instReprPlainTime : Repr PlainTime

Equations

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

def Std.Time.instDecidableEqPlainTime.decEq (x✝ x✝¹ : PlainTime) : Decidable (x✝ = x✝¹)

Equations

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

instance Std.Time.instDecidableEqPlainTime : DecidableEq PlainTime

Equations

• Std.Time.instDecidableEqPlainTime = Std.Time.instDecidableEqPlainTime.decEq

instance Std.Time.instInhabitedPlainTime : Inhabited PlainTime

Equations

• Std.Time.instInhabitedPlainTime = { default := { hour := 0, minute := 0, second := 0, nanosecond := ⟨0, Std.Time.instInhabitedPlainTime._proof_1⟩ } }

instance Std.Time.instOrdPlainTime : Ord PlainTime

Equations

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

theorem Std.Time.PlainTime.compare_def : compare = compareLex (compareOn fun (x : PlainTime) => x.hour) (compareLex (compareOn fun (x : PlainTime) => x.minute) (compareLex (compareOn fun (x : PlainTime) => x.second) (compareOn fun (x : PlainTime) => x.nanosecond)))

instance Std.Time.instTransOrdPlainTime : TransOrd PlainTime

instance Std.Time.instLawfulEqOrdPlainTime : LawfulEqOrd PlainTime

def Std.Time.PlainTime.midnight : PlainTime

Creates a PlainTime value representing midnight (00:00:00.000000000).

Equations

• Std.Time.PlainTime.midnight = { hour := 0, minute := 0, second := 0, nanosecond := 0 }

@[inline]

def Std.Time.PlainTime.ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) (nano : Nanosecond.Ordinal) : PlainTime

Creates a PlainTime value from the provided hours, minutes, seconds and nanoseconds components.

Equations

• Std.Time.PlainTime.ofHourMinuteSecondsNano hour minute second nano = { hour := hour, minute := minute, second := second, nanosecond := nano }

@[inline]

def Std.Time.PlainTime.ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : PlainTime

Creates a PlainTime value from the provided hours, minutes, and seconds.

Equations

• Std.Time.PlainTime.ofHourMinuteSeconds hour minute second = Std.Time.PlainTime.ofHourMinuteSecondsNano hour minute second 0

def Std.Time.PlainTime.toMilliseconds (time : PlainTime) : Millisecond.Offset

Converts a PlainTime value to the total number of milliseconds.

Equations

• time.toMilliseconds = time.hour.toOffset.toMilliseconds + time.minute.toOffset.toMilliseconds + time.second.toOffset.toMilliseconds + time.nanosecond.toOffset.toMilliseconds

def Std.Time.PlainTime.toNanoseconds (time : PlainTime) : Nanosecond.Offset

Converts a PlainTime value to the total number of nanoseconds.

Equations

• time.toNanoseconds = time.hour.toOffset.toNanoseconds + time.minute.toOffset.toNanoseconds + time.second.toOffset.toNanoseconds + time.nanosecond.toOffset

def Std.Time.PlainTime.toSeconds (time : PlainTime) : Second.Offset

Converts a PlainTime value to the total number of seconds.

Equations

• time.toSeconds = time.hour.toOffset.toSeconds + time.minute.toOffset.toSeconds + time.second.toOffset

def Std.Time.PlainTime.toMinutes (time : PlainTime) : Minute.Offset

Converts a PlainTime value to the total number of minutes.

Equations

• time.toMinutes = time.hour.toOffset.toMinutes + time.minute.toOffset + time.second.toOffset.toMinutes

def Std.Time.PlainTime.toHours (time : PlainTime) : Hour.Offset

Converts a PlainTime value to the total number of hours.

Equations

• time.toHours = time.hour.toOffset

def Std.Time.PlainTime.ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime

Creates a PlainTime value from a total number of nanoseconds.

Equations

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

@[inline]

def Std.Time.PlainTime.ofMilliseconds (millis : Millisecond.Offset) : PlainTime

Creates a PlainTime value from a total number of millisecond.

Equations

• Std.Time.PlainTime.ofMilliseconds millis = Std.Time.PlainTime.ofNanoseconds millis.toNanoseconds

@[inline]

def Std.Time.PlainTime.ofSeconds (secs : Second.Offset) : PlainTime

Creates a PlainTime value from a total number of seconds.

Equations

• Std.Time.PlainTime.ofSeconds secs = Std.Time.PlainTime.ofNanoseconds secs.toNanoseconds

@[inline]

def Std.Time.PlainTime.ofMinutes (secs : Minute.Offset) : PlainTime

Creates a PlainTime value from a total number of minutes.

Equations

• Std.Time.PlainTime.ofMinutes secs = Std.Time.PlainTime.ofNanoseconds secs.toNanoseconds

@[inline]

def Std.Time.PlainTime.ofHours (hour : Hour.Offset) : PlainTime

Creates a PlainTime value from a total number of hours.

Equations

• Std.Time.PlainTime.ofHours hour = Std.Time.PlainTime.ofNanoseconds hour.toNanoseconds

@[inline]

def Std.Time.PlainTime.addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime

Adds seconds to a PlainTime.

Equations

• time.addSeconds secondsToAdd = Std.Time.PlainTime.ofNanoseconds (time.toNanoseconds + secondsToAdd.toNanoseconds)

@[inline]

def Std.Time.PlainTime.subSeconds (time : PlainTime) (secondsToSub : Second.Offset) : PlainTime

Subtracts seconds from a PlainTime.

Equations

• time.subSeconds secondsToSub = time.addSeconds (-secondsToSub)

@[inline]

def Std.Time.PlainTime.addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime

Adds minutes to a PlainTime.

Equations

• time.addMinutes minutesToAdd = Std.Time.PlainTime.ofNanoseconds (time.toNanoseconds + minutesToAdd.toNanoseconds)

@[inline]

def Std.Time.PlainTime.subMinutes (time : PlainTime) (minutesToSub : Minute.Offset) : PlainTime

Subtracts minutes from a PlainTime.

Equations

• time.subMinutes minutesToSub = time.addMinutes (-minutesToSub)

@[inline]

def Std.Time.PlainTime.addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime

Adds hours to a PlainTime.

Equations

• time.addHours hoursToAdd = Std.Time.PlainTime.ofNanoseconds (time.toNanoseconds + hoursToAdd.toNanoseconds)

@[inline]

def Std.Time.PlainTime.subHours (time : PlainTime) (hoursToSub : Hour.Offset) : PlainTime

Subtracts hours from a PlainTime.

Equations

• time.subHours hoursToSub = time.addHours (-hoursToSub)

def Std.Time.PlainTime.addNanoseconds (time : PlainTime) (nanosToAdd : Nanosecond.Offset) : PlainTime

Adds nanoseconds to a PlainTime.

Equations

• time.addNanoseconds nanosToAdd = Std.Time.PlainTime.ofNanoseconds (time.toNanoseconds + nanosToAdd)

def Std.Time.PlainTime.subNanoseconds (time : PlainTime) (nanosToSub : Nanosecond.Offset) : PlainTime

Subtracts nanoseconds from a PlainTime.

Equations

• time.subNanoseconds nanosToSub = time.addNanoseconds (-nanosToSub)

def Std.Time.PlainTime.addMilliseconds (time : PlainTime) (millisToAdd : Millisecond.Offset) : PlainTime

Adds milliseconds to a PlainTime.

Equations

• time.addMilliseconds millisToAdd = Std.Time.PlainTime.ofMilliseconds (time.toMilliseconds + millisToAdd)

def Std.Time.PlainTime.subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : PlainTime

Subtracts milliseconds from a PlainTime.

Equations

• time.subMilliseconds millisToSub = time.addMilliseconds (-millisToSub)

@[inline]

def Std.Time.PlainTime.withSeconds (pt : PlainTime) (second : Second.Ordinal true) : PlainTime

Creates a new PlainTime by adjusting the second component to the given value.

Equations

• pt.withSeconds second = { hour := pt.hour, minute := pt.minute, second := second, nanosecond := pt.nanosecond }

@[inline]

def Std.Time.PlainTime.withMinutes (pt : PlainTime) (minute : Minute.Ordinal) : PlainTime

Creates a new PlainTime by adjusting the minute component to the given value.

Equations

• pt.withMinutes minute = { hour := pt.hour, minute := minute, second := pt.second, nanosecond := pt.nanosecond }

@[inline]

def Std.Time.PlainTime.withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime

Creates a new PlainTime by adjusting the milliseconds component inside the nano component of its time to the given value.

Equations

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

@[inline]

def Std.Time.PlainTime.withNanoseconds (pt : PlainTime) (nano : Nanosecond.Ordinal) : PlainTime

Creates a new PlainTime by adjusting the nano component to the given value.

Equations

• pt.withNanoseconds nano = { hour := pt.hour, minute := pt.minute, second := pt.second, nanosecond := nano }

@[inline]

def Std.Time.PlainTime.withHours (pt : PlainTime) (hour : Hour.Ordinal) : PlainTime

Creates a new PlainTime by adjusting the hour component to the given value.

Equations

• pt.withHours hour = { hour := hour, minute := pt.minute, second := pt.second, nanosecond := pt.nanosecond }

@[inline]

def Std.Time.PlainTime.millisecond (pt : PlainTime) : Millisecond.Ordinal

Millisecond component of the PlainTime

Equations

• pt.millisecond = Std.Time.Internal.Bounded.LE.ediv pt.nanosecond 1000000 Std.Time.PlainTime.millisecond._proof_1✝

instance Std.Time.PlainTime.instHAddOffset : HAdd PlainTime Nanosecond.Offset PlainTime

Equations

• Std.Time.PlainTime.instHAddOffset = { hAdd := Std.Time.PlainTime.addNanoseconds }

instance Std.Time.PlainTime.instHSubOffset : HSub PlainTime Nanosecond.Offset PlainTime

Equations

• Std.Time.PlainTime.instHSubOffset = { hSub := Std.Time.PlainTime.subNanoseconds }

instance Std.Time.PlainTime.instHAddOffset_1 : HAdd PlainTime Millisecond.Offset PlainTime

Equations

• Std.Time.PlainTime.instHAddOffset_1 = { hAdd := Std.Time.PlainTime.addMilliseconds }

instance Std.Time.PlainTime.instHSubOffset_1 : HSub PlainTime Millisecond.Offset PlainTime

Equations

• Std.Time.PlainTime.instHSubOffset_1 = { hSub := Std.Time.PlainTime.subMilliseconds }

instance Std.Time.PlainTime.instHAddOffset_2 : HAdd PlainTime Second.Offset PlainTime

Equations

• Std.Time.PlainTime.instHAddOffset_2 = { hAdd := Std.Time.PlainTime.addSeconds }

instance Std.Time.PlainTime.instHSubOffset_2 : HSub PlainTime Second.Offset PlainTime

Equations

• Std.Time.PlainTime.instHSubOffset_2 = { hSub := Std.Time.PlainTime.subSeconds }

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

Equations

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

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

Equations

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

instance Std.Time.PlainTime.instHAddOffset_4 : HAdd PlainTime Hour.Offset PlainTime

Equations

• Std.Time.PlainTime.instHAddOffset_4 = { hAdd := Std.Time.PlainTime.addHours }

instance Std.Time.PlainTime.instHSubOffset_4 : HSub PlainTime Hour.Offset PlainTime

Equations

• Std.Time.PlainTime.instHSubOffset_4 = { hSub := Std.Time.PlainTime.subHours }