structure Std.Time.Duration : Type

Represents a time interval with nanoseconds precision.

• second : Second.Offset

  Second offset of the duration.

• nano : Nanosecond.Span

  Nanosecond span that ranges from -999999999 and 999999999

• proof : self.second.val ≥ 0 ∧ self.nano.val ≥ 0 ∨ self.second.val ≤ 0 ∧ self.nano.val ≤ 0

  Proof that the duration is valid, ensuring that the second and nano values are correctly related.

theorem Std.Time.Duration.ext_iff {x y : Duration} : x = y ↔ x.second = y.second ∧ x.nano = y.nano

theorem Std.Time.Duration.ext {x y : Duration} (second : x.second = y.second) (nano : x.nano = y.nano) : x = y

instance Std.Time.instReprDuration : Repr Duration

instance Std.Time.instDecidableEqDuration : DecidableEq Duration

instance Std.Time.instToStringDuration : ToString Duration

def Std.Time.instToStringDuration.leftPad (n : Nat) (s : String) : String

instance Std.Time.instReprDuration_1 : Repr Duration

instance Std.Time.instInhabitedDuration : Inhabited Duration

instance Std.Time.instOfNatDuration {n : Nat} : OfNat Duration n

instance Std.Time.instOrdDuration : Ord Duration

theorem Std.Time.Duration.compare_def : compare = compareLex (compareOn fun (x : Duration) => x.second) (compareOn fun (x : Duration) => x.nano)

instance Std.Time.instTransOrdDuration : TransOrd Duration

instance Std.Time.instLawfulEqOrdDuration : LawfulEqOrd Duration

@[inline]

def Std.Time.Duration.neg (duration : Duration) : Duration

Negates a Duration, flipping its second and nanosecond values.

@[inline]

def Std.Time.Duration.ofSeconds (s : Second.Offset) : Duration

Creates a new Duration out of Second.Offset.

def Std.Time.Duration.ofNanoseconds (s : Nanosecond.Offset) : Duration

Creates a new Duration out of Nanosecond.Offset.

theorem Std.Time.Duration.ofNanoseconds.mod_nonpos {a : Int} (b : Int) : a ≤ 0 → b ≥ 0 → 0 ≥ a.tmod b

theorem Std.Time.Duration.ofNanoseconds.tdiv_neg {a b : Int} (Ha : a ≤ 0) (Hb : 0 ≤ b) : a.tdiv b ≤ 0

@[inline]

def Std.Time.Duration.ofMillisecond (s : Millisecond.Offset) : Duration

Creates a new Duration out of Millisecond.Offset.

@[inline]

def Std.Time.Duration.isZero (d : Duration) : Bool

Checks if the duration is zero seconds and zero nanoseconds.

@[inline]

def Std.Time.Duration.toSeconds (duration : Duration) : Second.Offset

Converts a Duration to a Second.Offset

@[inline]

def Std.Time.Duration.toMilliseconds (duration : Duration) : Millisecond.Offset

Converts a Duration to a Millisecond.Offset

@[inline]

def Std.Time.Duration.toNanoseconds (duration : Duration) : Nanosecond.Offset

Converts a Duration to a Nanosecond.Offset

instance Std.Time.Duration.instLE : LE Duration

instance Std.Time.Duration.instDecidableLe {x y : Duration} : Decidable (x ≤ y)

instance Std.Time.Duration.instLT : LT Duration

instance Std.Time.Duration.instDecidableLt {x y : Duration} : Decidable (x < y)

@[inline]

def Std.Time.Duration.toMinutes (tm : Duration) : Minute.Offset

Converts a Duration to a Minute.Offset

@[inline]

def Std.Time.Duration.toDays (tm : Duration) : Day.Offset

Converts a Duration to a Day.Offset

@[inline]

def Std.Time.Duration.fromComponents (secs : Second.Offset) (nanos : Nanosecond.Span) : Duration

Normalizes Second.Offset and NanoSecond.span in order to build a new Duration out of it.

@[inline]

def Std.Time.Duration.add (t₁ t₂ : Duration) : Duration

Adds two durations together, handling any carry-over in nanoseconds.

@[inline]

def Std.Time.Duration.sub (t₁ t₂ : Duration) : Duration

Subtracts one Duration from another.

@[inline]

def Std.Time.Duration.addNanoseconds (t : Duration) (s : Nanosecond.Offset) : Duration

Adds a Nanosecond.Offset to a Duration

@[inline]

def Std.Time.Duration.addMilliseconds (t : Duration) (s : Millisecond.Offset) : Duration

Adds a Millisecond.Offset to a Duration

@[inline]

def Std.Time.Duration.subMilliseconds (t : Duration) (s : Millisecond.Offset) : Duration

Adds a Millisecond.Offset to a Duration

@[inline]

def Std.Time.Duration.subNanoseconds (t : Duration) (s : Nanosecond.Offset) : Duration

Adds a Nanosecond.Offset to a Duration

@[inline]

def Std.Time.Duration.addSeconds (t : Duration) (s : Second.Offset) : Duration

Adds a Second.Offset to a Duration

@[inline]

def Std.Time.Duration.subSeconds (t : Duration) (s : Second.Offset) : Duration

Subtracts a Second.Offset from a Duration

@[inline]

def Std.Time.Duration.addMinutes (t : Duration) (m : Minute.Offset) : Duration

Adds a Minute.Offset to a Duration

@[inline]

def Std.Time.Duration.subMinutes (t : Duration) (m : Minute.Offset) : Duration

Subtracts a Minute.Offset from a Duration

@[inline]

def Std.Time.Duration.addHours (t : Duration) (h : Hour.Offset) : Duration

Adds an Hour.Offset to a Duration

@[inline]

def Std.Time.Duration.subHours (t : Duration) (h : Hour.Offset) : Duration

Subtracts an Hour.Offset from a Duration

@[inline]

def Std.Time.Duration.addDays (t : Duration) (d : Day.Offset) : Duration

Adds a Day.Offset to a Duration

@[inline]

def Std.Time.Duration.subDays (t : Duration) (d : Day.Offset) : Duration

Subtracts a Day.Offset from a Duration

@[inline]

def Std.Time.Duration.addWeeks (t : Duration) (w : Week.Offset) : Duration

Adds a Week.Offset to a Duration

@[inline]

def Std.Time.Duration.subWeeks (t : Duration) (w : Week.Offset) : Duration

Subtracts a Week.Offset from a Duration

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

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

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

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

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

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

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

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

instance Std.Time.Duration.instHAddOffset_4 : HAdd Duration Second.Offset Duration

instance Std.Time.Duration.instHSubOffset_4 : HSub Duration Second.Offset Duration

instance Std.Time.Duration.instHAddOffset_5 : HAdd Duration Nanosecond.Offset Duration

instance Std.Time.Duration.instHSubOffset_5 : HSub Duration Nanosecond.Offset Duration

instance Std.Time.Duration.instHAddOffset_6 : HAdd Duration Millisecond.Offset Duration

instance Std.Time.Duration.instHSubOffset_6 : HSub Duration Millisecond.Offset Duration

instance Std.Time.Duration.instHSub : HSub Duration Duration Duration

instance Std.Time.Duration.instHAdd : HAdd Duration Duration Duration

instance Std.Time.Duration.instCoeOffset : Coe Nanosecond.Offset Duration

instance Std.Time.Duration.instCoeOffset_1 : Coe Second.Offset Duration

instance Std.Time.Duration.instCoeOffset_2 : Coe Minute.Offset Duration

instance Std.Time.Duration.instCoeOffset_3 : Coe Hour.Offset Duration

instance Std.Time.Duration.instCoeOffset_4 : Coe Week.Offset Duration

instance Std.Time.Duration.instCoeOffset_5 : Coe Day.Offset Duration

instance Std.Time.Duration.instHMulInt : HMul Int Duration Duration

instance Std.Time.Duration.instHMulInt_1 : HMul Duration Int Duration

instance Std.Time.Duration.instHAddPlainTime : HAdd PlainTime Duration PlainTime

instance Std.Time.Duration.instHSubPlainTime : HSub PlainTime Duration PlainTime