def Std.Time.Millisecond.Ordinal : Type

Ordinal represents a bounded value for milliseconds, ranging from 0 to 999 milliseconds.

Equations

• Std.Time.Millisecond.Ordinal = Std.Time.Internal.Bounded.LE 0 999

instance Std.Time.Millisecond.instOrdinalRepr : Repr Ordinal

Equations

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

instance Std.Time.Millisecond.instOrdinalBEq : BEq Ordinal

Equations

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

instance Std.Time.Millisecond.instOrdinalLE : LE Ordinal

Equations

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

instance Std.Time.Millisecond.instOrdinalLT : LT Ordinal

Equations

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

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

Equations

• Std.Time.Millisecond.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 0 (0 + ↑999)) n)

instance Std.Time.Millisecond.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

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

Equations

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

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

Equations

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

def Std.Time.Millisecond.Offset : Type

Offset represents a duration offset in milliseconds.

Equations

• Std.Time.Millisecond.Offset = Std.Time.Internal.UnitVal (1 / 1000)

instance Std.Time.Millisecond.instOffsetRepr : Repr Offset

Equations

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

instance Std.Time.Millisecond.instOffsetBEq : BEq Offset

Equations

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

instance Std.Time.Millisecond.instOffsetInhabited : Inhabited Offset

Equations

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

instance Std.Time.Millisecond.instOffsetAdd : Add Offset

Equations

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

instance Std.Time.Millisecond.instOffsetSub : Sub Offset

Equations

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

instance Std.Time.Millisecond.instOffsetNeg : Neg Offset

Equations

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

instance Std.Time.Millisecond.instOffsetLE : LE Offset

Equations

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

instance Std.Time.Millisecond.instOffsetLT : LT Offset

Equations

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

instance Std.Time.Millisecond.instOffsetToString : ToString Offset

Equations

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

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

Equations

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

instance Std.Time.Millisecond.instDecidableLtOffset {x y : Offset} : Decidable (x < y)

Equations

• Std.Time.Millisecond.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

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

Equations

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

@[inline]

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

Creates an Offset from a natural number.

Equations

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

@[inline]

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

Creates an Offset from an integer.

Equations

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

@[inline]

def Std.Time.Millisecond.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 999) : Ordinal

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

Equations

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

@[inline]

def Std.Time.Millisecond.Ordinal.ofNat (data : Nat) (h : data ≤ 999) : Ordinal

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

Equations

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

@[inline]

def Std.Time.Millisecond.Ordinal.ofFin (data : Fin 1000) : Ordinal

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

Equations

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

@[inline]

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

Converts an Ordinal to an Offset.

Equations

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