Std.Time.Time.Unit.Hour

source

def Std.Time.Hour.Ordinal :

Type

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

Instances For

source

@[instance_reducible]

instance Std.Time.Hour.instReprOrdinal :

Repr Ordinal

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableEqOrdinal :

DecidableEq Ordinal

source

@[instance_reducible]

instance Std.Time.Hour.instLEOrdinal :

LE Ordinal

source

@[instance_reducible]

instance Std.Time.Hour.instLTOrdinal :

LT Ordinal

source

@[instance_reducible]

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

OfNat Ordinal n

source

@[instance_reducible]

instance Std.Time.Hour.instInhabitedOrdinal :

Inhabited Ordinal

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableLeOrdinal {x y : Ordinal} :

Decidable (x ≤ y)

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableLtOrdinal {x y : Ordinal} :

Decidable (x < y)

source

@[instance_reducible]

instance Std.Time.Hour.instOrdOrdinal :

Ord Ordinal

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.

Instances For

source

@[instance_reducible]

instance Std.Time.Hour.instReprOffset :

Repr Offset

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableEqOffset :

DecidableEq Offset

source

@[instance_reducible]

instance Std.Time.Hour.instInhabitedOffset :

Inhabited Offset

source

@[instance_reducible]

instance Std.Time.Hour.instAddOffset :

Add Offset

source

@[instance_reducible]

instance Std.Time.Hour.instSubOffset :

Sub Offset

source

@[instance_reducible]

instance Std.Time.Hour.instNegOffset :

Neg Offset

source

@[instance_reducible]

instance Std.Time.Hour.instToStringOffset :

ToString Offset

source

@[instance_reducible]

instance Std.Time.Hour.instLTOffset :

LT Offset

source

@[instance_reducible]

instance Std.Time.Hour.instLEOffset :

LE Offset

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableLeOffset {x y : Offset} :

Decidable (x ≤ y)

source

@[instance_reducible]

instance Std.Time.Hour.instDecidableLtOffset {x y : Offset} :

Decidable (x < y)

source

@[instance_reducible]

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

OfNat Offset n

source

@[instance_reducible]

instance Std.Time.Hour.instOrdOffset :

Ord Offset

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.

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.

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.

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.

Instances For

source

@[inline]

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

Ordinal

Creates an Ordinal from a Fin value.

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.

Instances For

source

@[inline]

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

Offset

Creates an Offset from a natural number.

Instances For

source

@[inline]

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

Offset

Creates an Offset from an integer.

Instances For