This module defines various units used for measuring, counting, and converting between hours, minutes, second, nanosecond, millisecond and nanoseconds.

The units are organized into types representing these time-related concepts, with operations provided to facilitate conversions and manipulations between them.

source
@[inline]
def Std.Time.Nanosecond.Offset.toMilliseconds (offset : Offset) :
Millisecond.Offset

Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.

Equations

- offset.toMilliseconds = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.toMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.div offset 1000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.ofMilliseconds (offset : Millisecond.Offset) :
Offset

Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.

Equations

- Std.Time.Nanosecond.Offset.ofMilliseconds offset = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 1000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.toSeconds (offset : Offset) :
Second.Offset

Converts a `Nanosecond.Offset` to a `Second.Offset`.

Equations

- offset.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.toSeconds._proof_1✝ (Std.Time.Internal.UnitVal.div offset 1000000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.ofSeconds (offset : Second.Offset) :
Offset

Converts a `Second.Offset` to a `Nanosecond.Offset`.

Equations

- Std.Time.Nanosecond.Offset.ofSeconds offset = Std.Time.Internal.UnitVal.mul offset 1000000000

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.toMinutes (offset : Offset) :
Minute.Offset

Converts a `Nanosecond.Offset` to a `Minute.Offset`.

Equations

- offset.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.toMinutes._proof_1✝ (Std.Time.Internal.UnitVal.div offset 60000000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.ofMinutes (offset : Minute.Offset) :
Offset

Converts a `Minute.Offset` to a `Nanosecond.Offset`.

Equations

- Std.Time.Nanosecond.Offset.ofMinutes offset = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60000000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.toHours (offset : Offset) :
Hour.Offset

Converts a `Nanosecond.Offset` to an `Hour.Offset`.

Equations

- offset.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.div offset 3600000000000)

Instances For

source
@[inline]
def Std.Time.Nanosecond.Offset.ofHours (offset : Hour.Offset) :
Offset

Converts an `Hour.Offset` to a `Nanosecond.Offset`.

Equations

- Std.Time.Nanosecond.Offset.ofHours offset = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600000000000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.toNanoseconds (offset : Offset) :
Nanosecond.Offset

Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.

Equations

- offset.toNanoseconds = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 1000000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.ofNanoseconds (offset : Nanosecond.Offset) :
Offset

Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.

Equations

- Std.Time.Millisecond.Offset.ofNanoseconds offset = offset.toMilliseconds

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.toSeconds (offset : Offset) :
Second.Offset

Converts a `Millisecond.Offset` to a `Second.Offset`.

Equations

- offset.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.toSeconds._proof_1✝ (Std.Time.Internal.UnitVal.div offset 1000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.ofSeconds (offset : Second.Offset) :
Offset

Converts a `Second.Offset` to a `Millisecond.Offset`.

Equations

- Std.Time.Millisecond.Offset.ofSeconds offset = Std.Time.Internal.UnitVal.mul offset 1000

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.toMinutes (offset : Offset) :
Minute.Offset

Converts a `Millisecond.Offset` to a `Minute.Offset`.

Equations

- offset.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.toMinutes._proof_1✝ (Std.Time.Internal.UnitVal.div offset 60000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.ofMinutes (offset : Minute.Offset) :
Offset

Converts a `Minute.Offset` to a `Millisecond.Offset`.

Equations

- Std.Time.Millisecond.Offset.ofMinutes offset = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.toHours (offset : Offset) :
Hour.Offset

Converts a `Millisecond.Offset` to an `Hour.Offset`.

Equations

- offset.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.div offset 3600000)

Instances For

source
@[inline]
def Std.Time.Millisecond.Offset.ofHours (offset : Hour.Offset) :
Offset

Converts an `Hour.Offset` to a `Millisecond.Offset`.

Equations

- Std.Time.Millisecond.Offset.ofHours offset = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600000)

Instances For

source
@[inline]
def Std.Time.Second.Offset.toNanoseconds (offset : Offset) :
Nanosecond.Offset

Converts a `Second.Offset` to a `Nanosecond.Offset`.

Equations

- offset.toNanoseconds = Std.Time.Internal.UnitVal.mul offset 1000000000

Instances For

source
@[inline]
def Std.Time.Second.Offset.ofNanoseconds (offset : Nanosecond.Offset) :
Offset

Converts a `Nanosecond.Offset` to a `Second.Offset`.

Equations

- Std.Time.Second.Offset.ofNanoseconds offset = offset.toSeconds

Instances For

source
@[inline]
def Std.Time.Second.Offset.toMilliseconds (offset : Offset) :
Millisecond.Offset

Converts a `Second.Offset` to a `Millisecond.Offset`.

Equations

- offset.toMilliseconds = Std.Time.Internal.UnitVal.mul offset 1000

Instances For

source
@[inline]
def Std.Time.Second.Offset.ofMilliseconds (offset : Millisecond.Offset) :
Offset

Converts a `Millisecond.Offset` to a `Second.Offset`.

Equations

- Std.Time.Second.Offset.ofMilliseconds offset = offset.toSeconds

Instances For

source
@[inline]
def Std.Time.Second.Offset.toMinutes (offset : Offset) :
Minute.Offset

Converts a `Second.Offset` to a `Minute.Offset`.

Equations

- offset.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.toMinutes._proof_1✝ (Std.Time.Internal.UnitVal.div offset 60)

Instances For

source
@[inline]
def Std.Time.Second.Offset.ofMinutes (offset : Minute.Offset) :
Offset

Converts a `Minute.Offset` to a `Second.Offset`.

Equations

- Std.Time.Second.Offset.ofMinutes offset = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60)

Instances For

source
@[inline]
def Std.Time.Second.Offset.toHours (offset : Offset) :
Hour.Offset

Converts a `Second.Offset` to an `Hour.Offset`.

Equations

- offset.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.div offset 3600)

Instances For

source
@[inline]
def Std.Time.Second.Offset.ofHours (offset : Hour.Offset) :
Offset

Converts an `Hour.Offset` to a `Second.Offset`.

Equations

- Std.Time.Second.Offset.ofHours offset = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600)

Instances For

source
@[inline]
def Std.Time.Minute.Offset.toNanoseconds (offset : Offset) :
Nanosecond.Offset

Converts a `Minute.Offset` to a `Nanosecond.Offset`.

Equations

- offset.toNanoseconds = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60000000000)

Instances For

source
@[inline]
def Std.Time.Minute.Offset.ofNanoseconds (offset : Nanosecond.Offset) :
Offset

Converts a `Nanosecond.Offset` to a `Minute.Offset`.

Equations

- Std.Time.Minute.Offset.ofNanoseconds offset = offset.toMinutes

Instances For

source
@[inline]
def Std.Time.Minute.Offset.toMilliseconds (offset : Offset) :
Millisecond.Offset

Converts a `Minute.Offset` to a `Millisecond.Offset`.

Equations

- offset.toMilliseconds = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60000)

Instances For

source
@[inline]
def Std.Time.Minute.Offset.ofMilliseconds (offset : Millisecond.Offset) :
Offset

Converts a `Millisecond.Offset` to a `Minute.Offset`.

Equations

- Std.Time.Minute.Offset.ofMilliseconds offset = offset.toMinutes

Instances For

source
@[inline]
def Std.Time.Minute.Offset.toSeconds (offset : Offset) :
Second.Offset

Converts a `Minute.Offset` to a `Second.Offset`.

Equations

- offset.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60)

Instances For

source
@[inline]
def Std.Time.Minute.Offset.ofSeconds (offset : Second.Offset) :
Offset

Converts a `Second.Offset` to a `Minute.Offset`.

Equations

- Std.Time.Minute.Offset.ofSeconds offset = offset.toMinutes

Instances For

source
@[inline]
def Std.Time.Minute.Offset.toHours (offset : Offset) :
Hour.Offset

Converts a `Minute.Offset` to an `Hour.Offset`.

Equations

- offset.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Minute.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.div offset 60)

Instances For

source
@[inline]
def Std.Time.Minute.Offset.ofHours (offset : Hour.Offset) :
Offset

Converts an `Hour.Offset` to a `Minute.Offset`.

Equations

- Std.Time.Minute.Offset.ofHours offset = Std.Time.Internal.UnitVal.cast Std.Time.Minute.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60)

Instances For

source
@[inline]
def Std.Time.Hour.Offset.toNanoseconds (offset : Offset) :
Nanosecond.Offset

Converts an `Hour.Offset` to a `Nanosecond.Offset`.

Equations

- offset.toNanoseconds = Std.Time.Internal.UnitVal.cast Std.Time.Nanosecond.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600000000000)

Instances For

source
@[inline]
def Std.Time.Hour.Offset.ofNanoseconds (offset : Nanosecond.Offset) :
Offset

Converts a `Nanosecond.Offset` to an `Hour.Offset`.

Equations

- Std.Time.Hour.Offset.ofNanoseconds offset = offset.toHours

Instances For

source
@[inline]
def Std.Time.Hour.Offset.toMilliseconds (offset : Offset) :
Millisecond.Offset

Converts an `Hour.Offset` to a `Millisecond.Offset`.

Equations

- offset.toMilliseconds = Std.Time.Internal.UnitVal.cast Std.Time.Millisecond.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600000)

Instances For

source
@[inline]
def Std.Time.Hour.Offset.ofMilliseconds (offset : Millisecond.Offset) :
Offset

Converts a `Millisecond.Offset` to an `Hour.Offset`.

Equations

- Std.Time.Hour.Offset.ofMilliseconds offset = offset.toHours

Instances For

source
@[inline]
def Std.Time.Hour.Offset.toSeconds (offset : Offset) :
Second.Offset

Converts an `Hour.Offset` to a `Second.Offset`.

Equations

- offset.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Second.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 3600)

Instances For

source
@[inline]
def Std.Time.Hour.Offset.ofSeconds (offset : Second.Offset) :
Offset

Converts a `Second.Offset` to an `Hour.Offset`.

Equations

- Std.Time.Hour.Offset.ofSeconds offset = offset.toHours

Instances For

source
@[inline]
def Std.Time.Hour.Offset.toMinutes (offset : Offset) :
Minute.Offset

Converts an `Hour.Offset` to a `Minute.Offset`.

Equations

- offset.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Minute.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.mul offset 60)

Instances For

source
@[inline]
def Std.Time.Hour.Offset.ofMinutes (offset : Minute.Offset) :
Offset

Converts a `Minute.Offset` to an `Hour.Offset`.

Equations

- Std.Time.Hour.Offset.ofMinutes offset = offset.toHours

Instances For