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

Instances For

• Std.Time.Hour.instInhabitedOrdinal
• Std.Time.Hour.instOfNatOrdinal
• Std.Time.Hour.instOrdinalBEq
• Std.Time.Hour.instOrdinalLE
• Std.Time.Hour.instOrdinalLT
• Std.Time.Hour.instOrdinalRepr

instance Std.Time.Hour.instOrdinalRepr : Repr Ordinal

Equations

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

instance Std.Time.Hour.instOrdinalBEq : BEq Ordinal

Equations

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

instance Std.Time.Hour.instOrdinalLE : LE Ordinal

Equations

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

instance Std.Time.Hour.instOrdinalLT : LT Ordinal

Equations

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

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

Equations

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

instance Std.Time.Hour.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Std.Time.Hour.Offset = Std.Time.Internal.UnitVal 3600

Instances For

• Std.Time.DateTime.instHAddOffset_2
• Std.Time.DateTime.instHSubOffset_2
• Std.Time.Duration.instCoeOffset_3
• Std.Time.Duration.instHAddOffset_2
• Std.Time.Duration.instHSubOffset_2
• Std.Time.Hour.instOfNatOffset
• Std.Time.Hour.instOffsetAdd
• Std.Time.Hour.instOffsetBEq
• Std.Time.Hour.instOffsetInhabited
• Std.Time.Hour.instOffsetNeg
• Std.Time.Hour.instOffsetRepr
• Std.Time.Hour.instOffsetSub
• Std.Time.Hour.instOffsetToString
• Std.Time.PlainDateTime.instHAddOffset_2
• Std.Time.PlainDateTime.instHSubOffset_2
• Std.Time.PlainTime.instHAddOffset_4
• Std.Time.PlainTime.instHSubOffset_4
• Std.Time.Timestamp.instHAddOffset_2
• Std.Time.Timestamp.instHSubOffset_2
• Std.Time.ZonedDateTime.instHAddOffset_2
• Std.Time.ZonedDateTime.instHSubOffset_2
• Std.Time.instHAddOffsetOffset_15
• Std.Time.instHAddOffsetOffset_21
• Std.Time.instHAddOffsetOffset_24
• Std.Time.instHAddOffsetOffset_25
• Std.Time.instHAddOffsetOffset_26
• Std.Time.instHAddOffsetOffset_27
• Std.Time.instHAddOffsetOffset_28
• Std.Time.instHAddOffsetOffset_29
• Std.Time.instHAddOffsetOffset_3
• Std.Time.instHAddOffsetOffset_34
• Std.Time.instHAddOffsetOffset_40
• Std.Time.instHAddOffsetOffset_9
• Std.Time.instHAddOffset_4
• Std.Time.instHSubOffsetOffset_15
• Std.Time.instHSubOffsetOffset_21
• Std.Time.instHSubOffsetOffset_24
• Std.Time.instHSubOffsetOffset_25
• Std.Time.instHSubOffsetOffset_26
• Std.Time.instHSubOffsetOffset_27
• Std.Time.instHSubOffsetOffset_28
• Std.Time.instHSubOffsetOffset_29
• Std.Time.instHSubOffsetOffset_3
• Std.Time.instHSubOffsetOffset_34
• Std.Time.instHSubOffsetOffset_40
• Std.Time.instHSubOffsetOffset_9
• Std.Time.instHSubOffset_4

instance Std.Time.Hour.instOffsetRepr : Repr Offset

Equations

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

instance Std.Time.Hour.instOffsetBEq : BEq Offset

Equations

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

instance Std.Time.Hour.instOffsetInhabited : Inhabited Offset

Equations

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

instance Std.Time.Hour.instOffsetAdd : Add Offset

Equations

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

instance Std.Time.Hour.instOffsetSub : Sub Offset

Equations

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

instance Std.Time.Hour.instOffsetNeg : Neg Offset

Equations

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

instance Std.Time.Hour.instOffsetToString : ToString Offset

Equations

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

instance Std.Time.Hour.instOfNatOffset {n : Nat} : OfNat 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) : 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 : Ordinal) : 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 : Ordinal) : 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) : Ordinal

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

Equations

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

@[inline]

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

Creates an Ordinal from a Fin value.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Std.Time.Hour.Offset.ofNat (data : Nat) : 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) : Offset

Creates an Offset from an integer.

Equations

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