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

@[implicit_reducible]

instance Std.Time.Millisecond.instReprOrdinal : Repr Ordinal

Equations

• Std.Time.Millisecond.instReprOrdinal = { reprPrec := Std.Time.Millisecond.instReprOrdinal._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instDecidableEqOrdinal : DecidableEq Ordinal

Equations

• Std.Time.Millisecond.instDecidableEqOrdinal = Std.Time.Millisecond.instDecidableEqOrdinal._aux_1

@[implicit_reducible]

instance Std.Time.Millisecond.instLEOrdinal : LE Ordinal

Equations

• Std.Time.Millisecond.instLEOrdinal = { le := Std.Time.Millisecond.instLEOrdinal._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instLTOrdinal : LT Ordinal

Equations

• Std.Time.Millisecond.instLTOrdinal = { lt := Std.Time.Millisecond.instLTOrdinal._aux_1 }

@[implicit_reducible]

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

Equations

• Std.Time.Millisecond.instOfNatOrdinal = { ofNat := Std.Time.Millisecond.instOfNatOrdinal._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

@[implicit_reducible]

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

Equations

• Std.Time.Millisecond.instDecidableLeOrdinal = Std.Time.Millisecond.instDecidableLeOrdinal._aux_1

@[implicit_reducible]

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

Equations

• Std.Time.Millisecond.instDecidableLtOrdinal = Std.Time.Millisecond.instDecidableLtOrdinal._aux_1

@[implicit_reducible]

instance Std.Time.Millisecond.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Millisecond.instOrdOrdinal = { compare := Std.Time.Millisecond.instOrdOrdinal._aux_1 }

instance Std.Time.Millisecond.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Millisecond.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Millisecond.Offset : Type

Offset represents a duration offset in milliseconds.

Equations

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

@[implicit_reducible]

instance Std.Time.Millisecond.instReprOffset : Repr Offset

Equations

• Std.Time.Millisecond.instReprOffset = { reprPrec := Std.Time.Millisecond.instReprOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.Millisecond.instDecidableEqOffset = Std.Time.Millisecond.instDecidableEqOffset._aux_1

@[implicit_reducible]

instance Std.Time.Millisecond.instInhabitedOffset : Inhabited Offset

Equations

• Std.Time.Millisecond.instInhabitedOffset = { default := Std.Time.Millisecond.instInhabitedOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instAddOffset : Add Offset

Equations

• Std.Time.Millisecond.instAddOffset = { add := Std.Time.Millisecond.instAddOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instSubOffset : Sub Offset

Equations

• Std.Time.Millisecond.instSubOffset = { sub := Std.Time.Millisecond.instSubOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instNegOffset : Neg Offset

Equations

• Std.Time.Millisecond.instNegOffset = { neg := Std.Time.Millisecond.instNegOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instLEOffset : LE Offset

Equations

• Std.Time.Millisecond.instLEOffset = { le := Std.Time.Millisecond.instLEOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instLTOffset : LT Offset

Equations

• Std.Time.Millisecond.instLTOffset = { lt := Std.Time.Millisecond.instLTOffset._aux_1 }

@[implicit_reducible]

instance Std.Time.Millisecond.instToStringOffset : ToString Offset

Equations

• Std.Time.Millisecond.instToStringOffset = { toString := Std.Time.Millisecond.instToStringOffset._aux_1 }

@[implicit_reducible]

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

Equations

• Std.Time.Millisecond.instDecidableLeOffset = Std.Time.Millisecond.instDecidableLeOffset._aux_1

@[implicit_reducible]

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

Equations

• Std.Time.Millisecond.instDecidableLtOffset = Std.Time.Millisecond.instDecidableLtOffset._aux_1

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Std.Time.Millisecond.instOrdOffset : Ord Offset

Equations

• Std.Time.Millisecond.instOrdOffset = { compare := Std.Time.Millisecond.instOrdOffset._aux_1 }

instance Std.Time.Millisecond.instTransOrdOffset : TransOrd Offset

instance Std.Time.Millisecond.instLawfulEqOrdOffset : LawfulEqOrd Offset

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