def Std.Time.Nanosecond.Ordinal : Type

Ordinal represents a nanosecond value that is bounded between 0 and 999,999,999 nanoseconds.

Equations

• Std.Time.Nanosecond.Ordinal = Std.Time.Internal.Bounded.LE 0 999999999

instance Std.Time.Nanosecond.instOrdinalRepr : Repr Ordinal

Equations

• Std.Time.Nanosecond.instOrdinalRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Nanosecond.instOrdinalBEq : BEq Ordinal

Equations

• Std.Time.Nanosecond.instOrdinalBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Nanosecond.instOrdinalLE : LE Ordinal

Equations

• Std.Time.Nanosecond.instOrdinalLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Nanosecond.instOrdinalLT : LT Ordinal

Equations

• Std.Time.Nanosecond.instOrdinalLT = Std.Time.Internal.Bounded.instLT

instance Std.Time.Nanosecond.instOfNatOrdinal {n : Nat} : OfNat Ordinal n

Equations

• Std.Time.Nanosecond.instOfNatOrdinal = { ofNat := Std.Time.Internal.Bounded.LE.ofFin (Fin.ofNat' (Nat.succ 999999999) n) }

instance Std.Time.Nanosecond.instInhabitedOrdinal : Inhabited Ordinal

Equations

• Std.Time.Nanosecond.instInhabitedOrdinal = { default := 0 }

instance Std.Time.Nanosecond.instDecidableLeOrdinal {x y : Ordinal} : Decidable (x ≤ y)

Equations

• Std.Time.Nanosecond.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Nanosecond.instDecidableLtOrdinal {x y : Ordinal} : Decidable (x < y)

Equations

• Std.Time.Nanosecond.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

def Std.Time.Nanosecond.Offset : Type

Offset represents a time offset in nanoseconds.

Equations

• Std.Time.Nanosecond.Offset = Std.Time.Internal.UnitVal (1 / 1000000000)

instance Std.Time.Nanosecond.instOffsetRepr : Repr Offset

Equations

• Std.Time.Nanosecond.instOffsetRepr = Std.Time.Internal.UnitVal.instRepr

instance Std.Time.Nanosecond.instOffsetBEq : BEq Offset

Equations

• Std.Time.Nanosecond.instOffsetBEq = Std.Time.Internal.instBEqUnitVal

instance Std.Time.Nanosecond.instOffsetInhabited : Inhabited Offset

Equations

• Std.Time.Nanosecond.instOffsetInhabited = Std.Time.Internal.instInhabitedUnitVal

instance Std.Time.Nanosecond.instOffsetAdd : Add Offset

Equations

• Std.Time.Nanosecond.instOffsetAdd = Std.Time.Internal.UnitVal.instAdd

instance Std.Time.Nanosecond.instOffsetSub : Sub Offset

Equations

• Std.Time.Nanosecond.instOffsetSub = Std.Time.Internal.UnitVal.instSub

instance Std.Time.Nanosecond.instOffsetNeg : Neg Offset

Equations

• Std.Time.Nanosecond.instOffsetNeg = Std.Time.Internal.UnitVal.instNeg

instance Std.Time.Nanosecond.instOffsetLE : LE Offset

Equations

• Std.Time.Nanosecond.instOffsetLE = Std.Time.Internal.UnitVal.instLE

instance Std.Time.Nanosecond.instOffsetLT : LT Offset

Equations

• Std.Time.Nanosecond.instOffsetLT = Std.Time.Internal.UnitVal.instLT

instance Std.Time.Nanosecond.instOffsetToString : ToString Offset

Equations

• Std.Time.Nanosecond.instOffsetToString = Std.Time.Internal.UnitVal.instToString

instance Std.Time.Nanosecond.instDecidableLeOffset {x y : Offset} : Decidable (x ≤ y)

Equations

• Std.Time.Nanosecond.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Nanosecond.instOfNatOffset {n : Nat} : OfNat Offset n

Equations

• Std.Time.Nanosecond.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }

@[inline]

def Std.Time.Nanosecond.Offset.ofNat (data : Nat) : Offset

Creates an Offset from a natural number.

Equations

• Std.Time.Nanosecond.Offset.ofNat data = { val := ↑data }

@[inline]

def Std.Time.Nanosecond.Offset.ofInt (data : Int) : Offset

Creates an Offset from an integer.

Equations

• Std.Time.Nanosecond.Offset.ofInt data = { val := data }

def Std.Time.Nanosecond.Span : Type

Span represents a bounded value for nanoseconds, ranging between -999999999 and 999999999. This can be used for operations that involve differences or adjustments within this range.

Equations

• Std.Time.Nanosecond.Span = Std.Time.Internal.Bounded.LE (-999999999) 999999999

instance Std.Time.Nanosecond.instSpanRepr : Repr Span

Equations

• Std.Time.Nanosecond.instSpanRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Nanosecond.instSpanBEq : BEq Span

Equations

• Std.Time.Nanosecond.instSpanBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Nanosecond.instSpanLE : LE Span

Equations

• Std.Time.Nanosecond.instSpanLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Nanosecond.instSpanLT : LT Span

Equations

• Std.Time.Nanosecond.instSpanLT = Std.Time.Internal.Bounded.instLT

instance Std.Time.Nanosecond.instInhabitedSpan : Inhabited Span

Equations

• Std.Time.Nanosecond.instInhabitedSpan = { default := Std.Time.Internal.Bounded.LE.mk 0 Std.Time.Nanosecond.instInhabitedSpan.proof_1 }

def Std.Time.Nanosecond.Span.toOffset (span : Span) : Offset

Creates a new Offset out of a Span.

Equations

• span.toOffset = { val := span.val }

def Std.Time.Nanosecond.Ordinal.OfDay : Type

Ordinal represents a bounded value for nanoseconds in a day, which ranges between 0 and 86400000000000.

Equations

• Std.Time.Nanosecond.Ordinal.OfDay = Std.Time.Internal.Bounded.LE 0 86400000000000

instance Std.Time.Nanosecond.Ordinal.instOfDayRepr : Repr OfDay

Equations

• Std.Time.Nanosecond.Ordinal.instOfDayRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Nanosecond.Ordinal.instOfDayBEq : BEq OfDay

Equations

• Std.Time.Nanosecond.Ordinal.instOfDayBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Nanosecond.Ordinal.instOfDayLE : LE OfDay

Equations

• Std.Time.Nanosecond.Ordinal.instOfDayLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Nanosecond.Ordinal.instOfDayLT : LT OfDay

Equations

• Std.Time.Nanosecond.Ordinal.instOfDayLT = Std.Time.Internal.Bounded.instLT

@[inline]

def Std.Time.Nanosecond.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 999999999) : Ordinal

Creates an Ordinal from an integer, ensuring the value is within bounds.

Equations

• Std.Time.Nanosecond.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

@[inline]

def Std.Time.Nanosecond.Ordinal.ofNat (data : Nat) (h : data ≤ 999999999) : Ordinal

Creates an Ordinal from a natural number, ensuring the value is within bounds.

Equations

• Std.Time.Nanosecond.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat data h

@[inline]

def Std.Time.Nanosecond.Ordinal.ofFin (data : Fin 1000000000) : Ordinal

Creates an Ordinal from a Fin, ensuring the value is within bounds.

Equations

• Std.Time.Nanosecond.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin data

@[inline]

def Std.Time.Nanosecond.Ordinal.toOffset (ordinal : Ordinal) : Offset

Converts an Ordinal to an Offset.

Equations

• ordinal.toOffset = { val := ordinal.val }