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.

Instances For

• Std.Time.DateTime.instHAddDuration
• Std.Time.DateTime.instHSubDuration
• Std.Time.DateTime.instHSubDuration_1
• Std.Time.Duration.instCoeOffset
• Std.Time.Duration.instCoeOffset_1
• Std.Time.Duration.instCoeOffset_2
• Std.Time.Duration.instCoeOffset_3
• Std.Time.Duration.instCoeOffset_4
• Std.Time.Duration.instCoeOffset_5
• Std.Time.Duration.instHAdd
• Std.Time.Duration.instHAddOffset
• Std.Time.Duration.instHAddOffset_1
• Std.Time.Duration.instHAddOffset_2
• Std.Time.Duration.instHAddOffset_3
• Std.Time.Duration.instHAddOffset_4
• Std.Time.Duration.instHAddOffset_5
• Std.Time.Duration.instHAddOffset_6
• Std.Time.Duration.instHAddPlainTime
• Std.Time.Duration.instHMulInt
• Std.Time.Duration.instHMulInt_1
• Std.Time.Duration.instHSub
• Std.Time.Duration.instHSubOffset
• Std.Time.Duration.instHSubOffset_1
• Std.Time.Duration.instHSubOffset_2
• Std.Time.Duration.instHSubOffset_3
• Std.Time.Duration.instHSubOffset_4
• Std.Time.Duration.instHSubOffset_5
• Std.Time.Duration.instHSubOffset_6
• Std.Time.Duration.instHSubPlainTime
• Std.Time.Duration.instLE
• Std.Time.PlainDate.instHSubDuration
• Std.Time.PlainDateTime.instHAddDuration
• Std.Time.PlainDateTime.instHSubDuration
• Std.Time.Timestamp.instHAddDuration
• Std.Time.Timestamp.instHSubDuration
• Std.Time.Timestamp.instHSubDuration_1
• Std.Time.ZonedDateTime.instHAddDuration
• Std.Time.ZonedDateTime.instHSubDuration
• Std.Time.ZonedDateTime.instHSubDuration_1
• Std.Time.instBEqDuration
• Std.Time.instInhabitedDuration
• Std.Time.instOfNatDuration
• Std.Time.instReprDuration
• Std.Time.instReprDuration_1
• Std.Time.instToStringDuration

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

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

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

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

@[inline]

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

Negates a Duration, flipping its second and nanosecond values.

@[inline]

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

Creates a new Duration out of Second.Offset.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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