structure Std.Time.Duration : Type

Represents a time interval with nanoseconds precision.

• second : Std.Time.Second.Offset

  Second offset of the duration.

• nano : Std.Time.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.

instance Std.Time.instReprDuration : Repr Std.Time.Duration

Equations

• Std.Time.instReprDuration = { reprPrec := Std.Time.reprDuration✝ }

instance Std.Time.instToStringDuration : ToString Std.Time.Duration

Equations

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

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

Equations

• Std.Time.instToStringDuration.leftPad n s = "".pushn '0' (n - s.length) ++ s

instance Std.Time.instReprDuration_1 : Repr Std.Time.Duration

Equations

• Std.Time.instReprDuration_1 = { reprPrec := fun (s : Std.Time.Duration) => reprPrec (toString s) }

instance Std.Time.instBEqDuration : BEq Std.Time.Duration

Equations

• Std.Time.instBEqDuration = { beq := fun (x y : Std.Time.Duration) => x.second == y.second && y.nano == x.nano }

instance Std.Time.instInhabitedDuration : Inhabited Std.Time.Duration

Equations

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

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

Equations

• Std.Time.instOfNatDuration = { ofNat := { second := Std.Time.Second.Offset.ofInt ↑n, nano := ⟨0, Std.Time.instOfNatDuration.proof_1⟩, proof := ⋯ } }

@[inline]

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

Negates a Duration, flipping its second and nanosecond values.

Equations

• duration.neg = { second := -duration.second, nano := Std.Time.Internal.Bounded.LE.neg duration.nano, proof := ⋯ }

@[inline]

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

Creates a new Duration out of Second.Offset.

Equations

• Std.Time.Duration.ofSeconds s = { second := s, nano := ⟨0, Std.Time.Duration.ofSeconds.proof_1⟩, proof := ⋯ }

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

Creates a new Duration out of Nanosecond.Offset.

Equations

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

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

@[inline]

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

Creates a new Duration out of Millisecond.Offset.

Equations

• Std.Time.Duration.ofMillisecond s = Std.Time.Duration.ofNanoseconds (Std.Time.Internal.UnitVal.mul s 1000000)

@[inline]

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

Checks if the duration is zero seconds and zero nanoseconds.

Equations

• d.isZero = decide (d.second.val = 0 ∧ d.nano.val = 0)

@[inline]

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

Converts a Duration to a Second.Offset

Equations

• duration.toSeconds = duration.second

@[inline]

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

Converts a Duration to a Millisecond.Offset

Equations

• duration.toMilliseconds = Std.Time.Internal.UnitVal.mul duration.second 1000 + { val := (Std.Time.Internal.Bounded.LE.ediv duration.nano 1000000 Std.Time.Duration.toMilliseconds.proof_1).val }

@[inline]

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

Converts a Duration to a Nanosecond.Offset

Equations

• duration.toNanoseconds = Std.Time.Internal.UnitVal.mul duration.second 1000000000 + { val := duration.nano.val }

instance Std.Time.Duration.instLE : LE Std.Time.Duration

Equations

• Std.Time.Duration.instLE = { le := fun (d1 d2 : Std.Time.Duration) => d1.toNanoseconds ≤ d2.toNanoseconds }

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

Equations

• Std.Time.Duration.instDecidableLe = inferInstanceAs (Decidable (x.toNanoseconds ≤ y.toNanoseconds))

@[inline]

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

Converts a Duration to a Minute.Offset

Equations

• tm.toMinutes = Std.Time.Internal.UnitVal.ediv tm.second 60

@[inline]

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

Converts a Duration to a Day.Offset

Equations

• tm.toDays = Std.Time.Internal.UnitVal.ediv tm.second 86400

@[inline]

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

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

Equations

• Std.Time.Duration.fromComponents secs nanos = Std.Time.Duration.ofNanoseconds (secs.toNanoseconds + nanos.toOffset)

@[inline]

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

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

Equations

• t₁.add t₂ = Std.Time.Duration.ofNanoseconds (t₁.toNanoseconds + t₂.toNanoseconds)

@[inline]

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

Subtracts one Duration from another.

Equations

• t₁.sub t₂ = t₁.add t₂.neg

@[inline]

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

Adds a Nanosecond.Offset to a Duration

Equations

• t.addNanoseconds s = t.add (Std.Time.Duration.ofNanoseconds s)

@[inline]

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

Adds a Millisecond.Offset to a Duration

Equations

• t.addMilliseconds s = t.add (Std.Time.Duration.ofNanoseconds s.toNanoseconds)

@[inline]

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

Adds a Millisecond.Offset to a Duration

Equations

• t.subMilliseconds s = t.sub (Std.Time.Duration.ofNanoseconds s.toNanoseconds)

@[inline]

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

Adds a Nanosecond.Offset to a Duration

Equations

• t.subNanoseconds s = t.sub (Std.Time.Duration.ofNanoseconds s)

@[inline]

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

Adds a Second.Offset to a Duration

Equations

• t.addSeconds s = t.add (Std.Time.Duration.ofSeconds s)

@[inline]

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

Subtracts a Second.Offset from a Duration

Equations

• t.subSeconds s = t.sub (Std.Time.Duration.ofSeconds s)

@[inline]

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

Adds a Minute.Offset to a Duration

Equations

• t.addMinutes m = t.addSeconds (Std.Time.Internal.UnitVal.mul m 60)

@[inline]

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

Subtracts a Minute.Offset from a Duration

Equations

• t.subMinutes m = t.subSeconds (Std.Time.Internal.UnitVal.mul m 60)

@[inline]

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

Adds an Hour.Offset to a Duration

Equations

• t.addHours h = t.addSeconds (Std.Time.Internal.UnitVal.mul h 3600)

@[inline]

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

Subtracts an Hour.Offset from a Duration

Equations

• t.subHours h = t.subSeconds (Std.Time.Internal.UnitVal.mul h 3600)

@[inline]

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

Adds a Day.Offset to a Duration

Equations

• t.addDays d = t.addSeconds (Std.Time.Internal.UnitVal.mul d 86400)

@[inline]

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

Subtracts a Day.Offset from a Duration

Equations

• t.subDays d = t.subSeconds (Std.Time.Internal.UnitVal.mul d 86400)

@[inline]

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

Adds a Week.Offset to a Duration

Equations

• t.addWeeks w = t.addSeconds (Std.Time.Internal.UnitVal.mul w 604800)

@[inline]

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

Subtracts a Week.Offset from a Duration

Equations

• t.subWeeks w = t.subSeconds (Std.Time.Internal.UnitVal.mul w 604800)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Std.Time.Duration.instHAddOffset_4 = { hAdd := Std.Time.Duration.addSeconds }

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

Equations

• Std.Time.Duration.instHSubOffset_4 = { hSub := Std.Time.Duration.subSeconds }

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

Equations

• Std.Time.Duration.instHAddOffset_5 = { hAdd := Std.Time.Duration.addNanoseconds }

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

Equations

• Std.Time.Duration.instHSubOffset_5 = { hSub := Std.Time.Duration.subNanoseconds }

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

Equations

• Std.Time.Duration.instHAddOffset_6 = { hAdd := Std.Time.Duration.addMilliseconds }

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

Equations

• Std.Time.Duration.instHSubOffset_6 = { hSub := Std.Time.Duration.subMilliseconds }

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

Equations

• Std.Time.Duration.instHSub = { hSub := Std.Time.Duration.sub }

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

Equations

• Std.Time.Duration.instHAdd = { hAdd := Std.Time.Duration.add }

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

Equations

• Std.Time.Duration.instCoeOffset = { coe := Std.Time.Duration.ofNanoseconds }

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

Equations

• Std.Time.Duration.instCoeOffset_1 = { coe := Std.Time.Duration.ofSeconds }

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

Equations

• Std.Time.Duration.instCoeOffset_2 = { coe := Std.Time.Duration.ofSeconds ∘ Std.Time.Minute.Offset.toSeconds }

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

Equations

• Std.Time.Duration.instCoeOffset_3 = { coe := Std.Time.Duration.ofSeconds ∘ Std.Time.Hour.Offset.toSeconds }

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

Equations

• Std.Time.Duration.instCoeOffset_4 = { coe := Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds ∘ Std.Time.Week.Offset.toDays }

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

Equations

• Std.Time.Duration.instCoeOffset_5 = { coe := Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds }

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

Equations

• Std.Time.Duration.instHMulInt = { hMul := fun (i : Int) (d : Std.Time.Duration) => Std.Time.Duration.ofNanoseconds (Std.Time.Nanosecond.Offset.ofInt (d.toNanoseconds.val * i)) }

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

Equations

• Std.Time.Duration.instHMulInt_1 = { hMul := fun (d : Std.Time.Duration) (i : Int) => Std.Time.Duration.ofNanoseconds (Std.Time.Nanosecond.Offset.ofInt (d.toNanoseconds.val * i)) }

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

Equations

• Std.Time.Duration.instHAddPlainTime = { hAdd := fun (pt : Std.Time.PlainTime) (d : Std.Time.Duration) => Std.Time.PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds) }

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

Equations

• Std.Time.Duration.instHSubPlainTime = { hSub := fun (pt : Std.Time.PlainTime) (d : Std.Time.Duration) => Std.Time.PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds) }