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

@[implicit_reducible]

instance Std.Time.instReprDuration :

def Std.Time.instReprDuration.repr :

Duration → Nat → Std.Format

Instances For

def Std.Time.instDecidableEqDuration.decEq (x✝ x✝¹ : Duration) :

Decidable (x✝ = x✝¹)

Instances For

@[implicit_reducible]

instance Std.Time.instDecidableEqDuration :

DecidableEq Duration

@[implicit_reducible]

instance Std.Time.instToStringDuration :

ToString Duration

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

Instances For

@[implicit_reducible]

instance Std.Time.instReprDuration_1 :

@[implicit_reducible]

instance Std.Time.instInhabitedDuration :

Inhabited Duration

@[implicit_reducible]

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

OfNat Duration n

@[implicit_reducible]

instance Std.Time.instOrdDuration :

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.

Instances For

@[inline]

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

Creates a new Duration out of Second.Offset.

Instances For

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

Creates a new Duration out of Nanosecond.Offset.

Instances For

@[inline]

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

Creates a new Duration out of Millisecond.Offset.

Instances For

@[inline]

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

Checks if the duration is zero seconds and zero nanoseconds.

Instances For

@[inline]

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

Converts a Duration to a Second.Offset

Instances For

@[inline]

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

Millisecond.Offset

Converts a Duration to a Millisecond.Offset

Instances For

@[inline]

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

Nanosecond.Offset

Converts a Duration to a Nanosecond.Offset

Instances For

@[implicit_reducible]

instance Std.Time.Duration.instLE :

@[implicit_reducible]

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

Decidable (x ≤ y)

@[implicit_reducible]

instance Std.Time.Duration.instLT :

@[implicit_reducible]

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

Decidable (x < y)

@[inline]

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

Converts a Duration to a Minute.Offset

Instances For

@[inline]

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

Converts a Duration to a Day.Offset

Instances For

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

Instances For

@[inline]

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

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

Instances For

@[inline]

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

Subtracts one Duration from another.

Instances For

@[inline]

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

Adds a Nanosecond.Offset to a Duration

Instances For

@[inline]

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

Adds a Millisecond.Offset to a Duration

Instances For

@[inline]

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

Adds a Millisecond.Offset to a Duration

Instances For

@[inline]

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

Adds a Nanosecond.Offset to a Duration

Instances For

@[inline]

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

Adds a Second.Offset to a Duration

Instances For

@[inline]

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

Subtracts a Second.Offset from a Duration

Instances For

@[inline]

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

Adds a Minute.Offset to a Duration

Instances For

@[inline]

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

Subtracts a Minute.Offset from a Duration

Instances For

@[inline]

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

Adds an Hour.Offset to a Duration

Instances For

@[inline]

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

Subtracts an Hour.Offset from a Duration

Instances For

@[inline]

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

Adds a Day.Offset to a Duration

Instances For

@[inline]

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

Subtracts a Day.Offset from a Duration

Instances For

@[inline]

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

Adds a Week.Offset to a Duration

Instances For

@[inline]

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

Subtracts a Week.Offset from a Duration

Instances For

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset :

HAdd Duration Day.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset :

HSub Duration Day.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_1 :

HAdd Duration Week.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_1 :

HSub Duration Week.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_2 :

HAdd Duration Hour.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_2 :

HSub Duration Hour.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_3 :

HAdd Duration Minute.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_3 :

HSub Duration Minute.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_4 :

HAdd Duration Second.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_4 :

HSub Duration Second.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_5 :

HAdd Duration Nanosecond.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_5 :

HSub Duration Nanosecond.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddOffset_6 :

HAdd Duration Millisecond.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSubOffset_6 :

HSub Duration Millisecond.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHSub :

HSub Duration Duration Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAdd :

HAdd Duration Duration Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset :

Coe Nanosecond.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset_1 :

Coe Second.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset_2 :

Coe Minute.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset_3 :

Coe Hour.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset_4 :

Coe Week.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instCoeOffset_5 :

Coe Day.Offset Duration

@[implicit_reducible]

instance Std.Time.Duration.instHMulInt :

HMul Int Duration Duration

@[implicit_reducible]

instance Std.Time.Duration.instHMulInt_1 :

HMul Duration Int Duration

@[implicit_reducible]

instance Std.Time.Duration.instHAddPlainTime :

HAdd PlainTime Duration PlainTime

@[implicit_reducible]

instance Std.Time.Duration.instHSubPlainTime :

HSub PlainTime Duration PlainTime