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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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