def Std.Time.Hour.Ordinal : Type

Ordinal represents a bounded value for hours, ranging from 0 to 23.

Equations

• Std.Time.Hour.Ordinal = Std.Time.Internal.Bounded.LE 0 23

instance Std.Time.Hour.instOrdinalRepr : Repr Std.Time.Hour.Ordinal

Equations

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

instance Std.Time.Hour.instOrdinalBEq : BEq Std.Time.Hour.Ordinal

instance Std.Time.Hour.instOrdinalLE : LE Std.Time.Hour.Ordinal

Equations

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

instance Std.Time.Hour.instOrdinalLT : LT Std.Time.Hour.Ordinal

Equations

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

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

instance Std.Time.Hour.instInhabitedOrdinal : Inhabited Std.Time.Hour.Ordinal

Equations

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

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

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

def Std.Time.Hour.Offset : Type

Offset represents an offset in hours, defined as an Int. This can be used to express durations or differences in hours.

instance Std.Time.Hour.instOffsetRepr : Repr Std.Time.Hour.Offset

instance Std.Time.Hour.instOffsetBEq : BEq Std.Time.Hour.Offset

Equations

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

instance Std.Time.Hour.instOffsetInhabited : Inhabited Std.Time.Hour.Offset

instance Std.Time.Hour.instOffsetAdd : Add Std.Time.Hour.Offset

Equations

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

instance Std.Time.Hour.instOffsetSub : Sub Std.Time.Hour.Offset

Equations

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

instance Std.Time.Hour.instOffsetNeg : Neg Std.Time.Hour.Offset

Equations

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

instance Std.Time.Hour.instOffsetToString : ToString Std.Time.Hour.Offset

Equations

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

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

Equations

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

@[inline]

def Std.Time.Hour.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 23) : Std.Time.Hour.Ordinal

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

Equations

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

def Std.Time.Hour.Ordinal.toRelative (ordinal : Std.Time.Hour.Ordinal) : Std.Time.Internal.Bounded.LE 1 12

Converts an Ordinal into a relative hour in the range of 1 to 12.

Equations

• ordinal.toRelative = ((Std.Time.Internal.Bounded.LE.add ordinal 11).emod 12 Std.Time.Hour.Ordinal.toRelative.proof_1).add 1

def Std.Time.Hour.Ordinal.shiftTo1BasedHour (ordinal : Std.Time.Hour.Ordinal) : Std.Time.Internal.Bounded.LE 1 24

Converts an Ordinal into a 1-based hour representation within the range of 1 to 24.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Time.Hour.Ordinal.ofNat (data : Nat) (h : data ≤ 23) : Std.Time.Hour.Ordinal

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

@[inline]

def Std.Time.Hour.Ordinal.ofFin (data : Fin 24) : Std.Time.Hour.Ordinal

Creates an Ordinal from a Fin value.

@[inline]

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

Converts an Ordinal to an Offset, which represents the duration in hours as an integer value.

@[inline]

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

Creates an Offset from a natural number.

Equations

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

@[inline]

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

Creates an Offset from an integer.

Equations

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