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

Instances For

source
theorem Std.Time.Duration.ext_iff {x y : Duration} :
x = y ↔ x.second = y.second ∧ x.nano = y.nano
source
theorem Std.Time.Duration.ext {x y : Duration} (second : x.second = y.second) (nano : x.nano = y.nano) :
x = y
source
instance Std.Time.instReprDuration :
Repr Duration
Equations

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

source
def Std.Time.instReprDuration.repr :
Duration → Nat → Std.Format
Equations

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

Instances For

source
def Std.Time.instDecidableEqDuration.decEq (x✝ x✝¹ : Duration) :
Decidable (x✝ = x✝¹)
Equations

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

Instances For

source
instance Std.Time.instDecidableEqDuration :
DecidableEq Duration
Equations

- Std.Time.instDecidableEqDuration = Std.Time.instDecidableEqDuration.decEq

source
instance Std.Time.instToStringDuration :
ToString Duration
Equations

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

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

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

Instances For

source
instance Std.Time.instReprDuration_1 :
Repr Duration
Equations

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

source
instance Std.Time.instInhabitedDuration :
Inhabited Duration
Equations

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

source
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.instInhabitedDuration._proof_1⟩, proof := ⋯ } }

source
instance Std.Time.instOrdDuration :
Ord Duration
Equations

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

source
theorem Std.Time.Duration.compare_def :
compare = compareLex (compareOn fun (x : Duration) => x.second) (compareOn fun (x : Duration) => x.nano)
source
instance Std.Time.instTransOrdDuration :
TransOrd Duration
source
instance Std.Time.instLawfulEqOrdDuration :
LawfulEqOrd Duration
source
@[inline]
def Std.Time.Duration.neg (duration : 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 := ⋯ }

Instances For

source
@[inline]
def Std.Time.Duration.ofSeconds (s : Second.Offset) :
Duration

Creates a new `Duration` out of `Second.Offset`.

Equations

- Std.Time.Duration.ofSeconds s = { second := s, nano := ⟨0, Std.Time.instInhabitedDuration._proof_1⟩, proof := ⋯ }

Instances For

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

Creates a new `Duration` out of `Nanosecond.Offset`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.ofMillisecond (s : Millisecond.Offset) :
Duration

Creates a new `Duration` out of `Millisecond.Offset`.

Equations

- Std.Time.Duration.ofMillisecond s = Std.Time.Duration.ofNanoseconds s.toNanoseconds

Instances For

source
@[inline]
def Std.Time.Duration.isZero (d : Duration) :
Bool

Checks if the duration is zero seconds and zero nanoseconds.

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.toSeconds (duration : Duration) :
Second.Offset

Converts a `Duration` to a `Second.Offset`

Equations

- duration.toSeconds = duration.second

Instances For

source
@[inline]
def Std.Time.Duration.toMilliseconds (duration : Duration) :
Millisecond.Offset

Converts a `Duration` to a `Millisecond.Offset`

Equations

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

Instances For

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

Instances For

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

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

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

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

source
instance Std.Time.Duration.instLT :
LT Duration
Equations

- Std.Time.Duration.instLT = { lt := fun (d1 d2 : Std.Time.Duration) => d1.toNanoseconds < d2.toNanoseconds }

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

- Std.Time.Duration.instDecidableLt = inferInstanceAs (Decidable (x.toNanoseconds < y.toNanoseconds))

source
@[inline]
def Std.Time.Duration.toMinutes (tm : Duration) :
Minute.Offset

Converts a `Duration` to a `Minute.Offset`

Equations

- tm.toMinutes = tm.second.toMinutes

Instances For

source
@[inline]
def Std.Time.Duration.toDays (tm : Duration) :
Day.Offset

Converts a `Duration` to a `Day.Offset`

Equations

- tm.toDays = tm.second.toDays

Instances For

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

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.add (t₁ t₂ : Duration) :
Duration

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

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.sub (t₁ t₂ : Duration) :
Duration

Subtracts one `Duration` from another.

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.addNanoseconds (t : Duration) (s : Nanosecond.Offset) :
Duration

Adds a `Nanosecond.Offset` to a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.addMilliseconds (t : Duration) (s : Millisecond.Offset) :
Duration

Adds a `Millisecond.Offset` to a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.subMilliseconds (t : Duration) (s : Millisecond.Offset) :
Duration

Adds a `Millisecond.Offset` to a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.subNanoseconds (t : Duration) (s : Nanosecond.Offset) :
Duration

Adds a `Nanosecond.Offset` to a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.addSeconds (t : Duration) (s : Second.Offset) :
Duration

Adds a `Second.Offset` to a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.subSeconds (t : Duration) (s : Second.Offset) :
Duration

Subtracts a `Second.Offset` from a `Duration`

Equations

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

Instances For

source
@[inline]
def Std.Time.Duration.addMinutes (t : Duration) (m : Minute.Offset) :
Duration

Adds a `Minute.Offset` to a `Duration`

Equations

- t.addMinutes m = t.addSeconds m.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.subMinutes (t : Duration) (m : Minute.Offset) :
Duration

Subtracts a `Minute.Offset` from a `Duration`

Equations

- t.subMinutes m = t.subSeconds m.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.addHours (t : Duration) (h : Hour.Offset) :
Duration

Adds an `Hour.Offset` to a `Duration`

Equations

- t.addHours h = t.addSeconds h.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.subHours (t : Duration) (h : Hour.Offset) :
Duration

Subtracts an `Hour.Offset` from a `Duration`

Equations

- t.subHours h = t.subSeconds h.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.addDays (t : Duration) (d : Day.Offset) :
Duration

Adds a `Day.Offset` to a `Duration`

Equations

- t.addDays d = t.addSeconds d.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.subDays (t : Duration) (d : Day.Offset) :
Duration

Subtracts a `Day.Offset` from a `Duration`

Equations

- t.subDays d = t.subSeconds d.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.addWeeks (t : Duration) (w : Week.Offset) :
Duration

Adds a `Week.Offset` to a `Duration`

Equations

- t.addWeeks w = t.addSeconds w.toSeconds

Instances For

source
@[inline]
def Std.Time.Duration.subWeeks (t : Duration) (w : Week.Offset) :
Duration

Subtracts a `Week.Offset` from a `Duration`

Equations

- t.subWeeks w = t.subSeconds w.toSeconds

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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