Documentation

Std.Time.Duration

structure Std.Time.Duration :

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.

Instances For

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 :

Equations

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

instance Std.Time.instDecidableEqDuration :

DecidableEq Duration

Equations

Std.Time.instDecidableEqDuration = Std.Time.decEqDuration✝

instance Std.Time.instToStringDuration :

ToString Duration

Equations

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

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

Equations

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

instance Std.Time.instReprDuration_1 :

Equations

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

instance Std.Time.instInhabitedDuration :

Inhabited Duration

Equations

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

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

OfNat Duration n

Equations

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

instance Std.Time.instOrdDuration :

Equations

Std.Time.instOrdDuration = { compare := compareLex (compareOn fun (x : Std.Time.Duration) => x.second) (compareOn fun (x : Std.Time.Duration) => x.nano) }

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) :

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 : Second.Offset) :

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 : Nanosecond.Offset) :

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

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) :

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 : Duration) :

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 : Duration) :

Converts a Duration to a Second.Offset

Equations

duration.toSeconds = duration.second

@[inline]

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

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 : Duration) :

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 :

Equations

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

instance Std.Time.Duration.instDecidableLe {x y : Duration} :

Decidable (x ≤ y)

Equations

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

@[inline]

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

Converts a Duration to a Minute.Offset

Equations

tm.toMinutes = Std.Time.Internal.UnitVal.tdiv tm.second 60

@[inline]

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

Converts a Duration to a Day.Offset

Equations

tm.toDays = Std.Time.Internal.UnitVal.tdiv tm.second 86400

@[inline]

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

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₂ : 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₂ : Duration) :

Subtracts one Duration from another.

Equations

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

@[inline]

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

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 : Duration) (s : Millisecond.Offset) :

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 : Duration) (s : Millisecond.Offset) :

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 : Duration) (s : Nanosecond.Offset) :

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 : Duration) (s : Second.Offset) :

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 : Duration) (s : Second.Offset) :

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 : Duration) (m : Minute.Offset) :

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 : Duration) (m : Minute.Offset) :

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 : Duration) (h : Hour.Offset) :

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 : Duration) (h : Hour.Offset) :

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 : Duration) (d : Day.Offset) :

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 : Duration) (d : Day.Offset) :

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 : Duration) (w : Week.Offset) :

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 : Duration) (w : Week.Offset) :

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 Duration Day.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset :

HSub Duration Day.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_1 :

HAdd Duration Week.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_1 :

HSub Duration Week.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_2 :

HAdd Duration Hour.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_2 :

HSub Duration Hour.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_3 :

HAdd Duration Minute.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_3 :

HSub Duration Minute.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_4 :

HAdd Duration Second.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_4 :

HSub Duration Second.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_5 :

HAdd Duration Nanosecond.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_5 :

HSub Duration Nanosecond.Offset Duration

Equations

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

instance Std.Time.Duration.instHAddOffset_6 :

HAdd Duration Millisecond.Offset Duration

Equations

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

instance Std.Time.Duration.instHSubOffset_6 :

HSub Duration Millisecond.Offset Duration

Equations

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

instance Std.Time.Duration.instHSub :

HSub Duration Duration Duration

Equations

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

instance Std.Time.Duration.instHAdd :

HAdd Duration Duration Duration

Equations

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

instance Std.Time.Duration.instCoeOffset :

Coe Nanosecond.Offset Duration

Equations

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

instance Std.Time.Duration.instCoeOffset_1 :

Coe Second.Offset Duration

Equations

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

instance Std.Time.Duration.instCoeOffset_2 :

Coe Minute.Offset Duration

Equations

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

instance Std.Time.Duration.instCoeOffset_3 :

Coe Hour.Offset Duration

Equations

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

instance Std.Time.Duration.instCoeOffset_4 :

Coe Week.Offset 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 Day.Offset Duration

Equations

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

instance Std.Time.Duration.instHMulInt :

HMul Int Duration 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 Duration Int 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 PlainTime Duration 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 PlainTime Duration PlainTime

Equations

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