source
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

source
instance Std.Time.Hour.instReprOrdinal :
Repr Ordinal
Equations

- Std.Time.Hour.instReprOrdinal = Std.Time.Internal.Bounded.instRepr

source
instance Std.Time.Hour.instDecidableEqOrdinal :
DecidableEq Ordinal
Equations

- Std.Time.Hour.instDecidableEqOrdinal = Std.Time.Internal.Bounded.instDecidableEq

source
instance Std.Time.Hour.instLEOrdinal :
LE Ordinal
Equations

- Std.Time.Hour.instLEOrdinal = Std.Time.Internal.Bounded.instLE

source
instance Std.Time.Hour.instLTOrdinal :
LT Ordinal
Equations

- Std.Time.Hour.instLTOrdinal = Std.Time.Internal.Bounded.instLT

source
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)

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

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

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

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

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

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

source
instance Std.Time.Hour.instOrdOrdinal :
Ord Ordinal
Equations

- Std.Time.Hour.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 0 23))

source
instance Std.Time.Hour.instTransOrdOrdinal :
TransOrd Ordinal
source
instance Std.Time.Hour.instLawfulEqOrdOrdinal :
LawfulEqOrd Ordinal
source
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

source
instance Std.Time.Hour.instReprOffset :
Repr Offset
Equations

- Std.Time.Hour.instReprOffset = Std.Time.Internal.UnitVal.instRepr

source
instance Std.Time.Hour.instDecidableEqOffset :
DecidableEq Offset
Equations

- Std.Time.Hour.instDecidableEqOffset = Std.Time.Internal.instDecidableEqUnitVal

source
instance Std.Time.Hour.instInhabitedOffset :
Inhabited Offset
Equations

- Std.Time.Hour.instInhabitedOffset = Std.Time.Internal.instInhabitedUnitVal

source
instance Std.Time.Hour.instAddOffset :
Add Offset
Equations

- Std.Time.Hour.instAddOffset = Std.Time.Internal.UnitVal.instAdd

source
instance Std.Time.Hour.instSubOffset :
Sub Offset
Equations

- Std.Time.Hour.instSubOffset = Std.Time.Internal.UnitVal.instSub

source
instance Std.Time.Hour.instNegOffset :
Neg Offset
Equations

- Std.Time.Hour.instNegOffset = Std.Time.Internal.UnitVal.instNeg

source
instance Std.Time.Hour.instToStringOffset :
ToString Offset
Equations

- Std.Time.Hour.instToStringOffset = Std.Time.Internal.UnitVal.instToString

source
instance Std.Time.Hour.instLTOffset :
LT Offset
Equations

- Std.Time.Hour.instLTOffset = Std.Time.Internal.UnitVal.instLT

source
instance Std.Time.Hour.instLEOffset :
LE Offset
Equations

- Std.Time.Hour.instLEOffset = Std.Time.Internal.UnitVal.instLE

source
instance Std.Time.Hour.instDecidableLeOffset {x y : Offset} :
Decidable (x ≤ y)
Equations

- Std.Time.Hour.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Hour.instDecidableLtOffset {x y : Offset} :
Decidable (x < y)
Equations

- Std.Time.Hour.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

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

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

source
instance Std.Time.Hour.instOrdOffset :
Ord Offset
Equations

- Std.Time.Hour.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal 3600))

source
instance Std.Time.Hour.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.Hour.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
@[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

Instances For

source
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

Instances For

source
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.

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For