def Std.Time.Minute.Ordinal : Type

Ordinal represents a bounded value for minutes, ranging from 0 to 59. This is useful for representing the minute component of a time.

Equations

• Std.Time.Minute.Ordinal = Std.Time.Internal.Bounded.LE 0 59

instance Std.Time.Minute.instOrdinalRepr : Repr Ordinal

Equations

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

instance Std.Time.Minute.instOrdinalBEq : BEq Ordinal

Equations

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

instance Std.Time.Minute.instOrdinalLE : LE Ordinal

Equations

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

instance Std.Time.Minute.instOrdinalLT : LT Ordinal

Equations

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

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

Equations

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

instance Std.Time.Minute.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

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

Equations

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

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

Equations

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

def Std.Time.Minute.Offset : Type

Offset represents a duration offset in minutes.

Equations

• Std.Time.Minute.Offset = Std.Time.Internal.UnitVal 60

instance Std.Time.Minute.instOffsetRepr : Repr Offset

Equations

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

instance Std.Time.Minute.instOffsetBEq : BEq Offset

Equations

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

instance Std.Time.Minute.instOffsetInhabited : Inhabited Offset

Equations

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

instance Std.Time.Minute.instOffsetAdd : Add Offset

Equations

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

instance Std.Time.Minute.instOffsetSub : Sub Offset

Equations

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

instance Std.Time.Minute.instOffsetNeg : Neg Offset

Equations

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

instance Std.Time.Minute.instOffsetToString : ToString Offset

Equations

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

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

Equations

• Std.Time.Minute.instOfNatOffset = { ofNat := { val := Int.ofNat n } }

@[inline]

def Std.Time.Minute.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 59) : Ordinal

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

Equations

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

@[inline]

def Std.Time.Minute.Ordinal.ofNat (data : Nat) (h : data ≤ 59) : Ordinal

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

Equations

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

@[inline]

def Std.Time.Minute.Ordinal.ofFin (data : Fin 60) : Ordinal

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

Equations

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

@[inline]

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

Converts an Ordinal to an Offset.

Equations

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

@[inline]

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

Creates an Offset from a natural number.

Equations

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

@[inline]

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

Creates an Offset from an integer.

Equations

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