def Std.Time.Second.Ordinal (leap : Bool) : Type

Ordinal represents a bounded value for second, which ranges between 0 and 59 or 60. This accounts for potential leap second.

instance Std.Time.Second.instLEOrdinal {leap : Bool} : LE (Ordinal leap)

instance Std.Time.Second.instLTOrdinal {leap : Bool} : LT (Ordinal leap)

instance Std.Time.Second.instReprOrdinal {leap : Bool} : Repr (Ordinal leap)

instance Std.Time.Second.instToStringOrdinal {leap : Bool} : ToString (Ordinal leap)

instance Std.Time.Second.instOfNatOrdinal {leap : Bool} {n : Nat} : OfNat (Ordinal leap) n

instance Std.Time.Second.instDecidableLeOrdinal {leap : Bool} {x y : Ordinal leap} : Decidable (x ≤ y)

instance Std.Time.Second.instDecidableLtOrdinal {leap : Bool} {x y : Ordinal leap} : Decidable (x < y)

instance Std.Time.Second.instDecidableEqOrdinal {leap : Bool} : DecidableEq (Ordinal leap)

instance Std.Time.Second.instOrdOrdinal {leap : Bool} : Ord (Ordinal leap)

instance Std.Time.Second.instTransOrdOrdinal {leap : Bool} : TransOrd (Ordinal leap)

instance Std.Time.Second.instLawfulEqOrdOrdinal {leap : Bool} : LawfulEqOrd (Ordinal leap)

def Std.Time.Second.Offset : Type

Offset represents an offset in seconds. It is defined as an Int.

instance Std.Time.Second.instOffsetRepr : Repr Offset

instance Std.Time.Second.instOffsetDecidableEq : DecidableEq Offset

instance Std.Time.Second.instOffsetInhabited : Inhabited Offset

instance Std.Time.Second.instOffsetAdd : Add Offset

instance Std.Time.Second.instOffsetSub : Sub Offset

instance Std.Time.Second.instOffsetNeg : Neg Offset

instance Std.Time.Second.instOffsetLE : LE Offset

instance Std.Time.Second.instOffsetLT : LT Offset

instance Std.Time.Second.instOffsetToString : ToString Offset

instance Std.Time.Second.instDecidableLeOffset {x y : Offset} : Decidable (x ≤ y)

instance Std.Time.Second.instDecidableLtOffset {x y : Offset} : Decidable (x < y)

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

instance Std.Time.Second.instOrdOffset : Ord Offset

instance Std.Time.Second.instTransOrdOffset : TransOrd Offset

instance Std.Time.Second.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

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

Creates an Second.Offset from a natural number.

@[inline]

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

Creates an Second.Offset from an integer.

@[inline]

def Std.Time.Second.Ordinal.ofInt {leap : Bool} (data : Int) (h : 0 ≤ data ∧ data ≤ Int.ofNat (if leap = true then 60 else 59)) : Ordinal leap

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

@[inline]

def Std.Time.Second.Ordinal.ofNat {leap : Bool} (data : Nat) (h : data ≤ if leap = true then 60 else 59) : Ordinal leap

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

@[inline]

def Std.Time.Second.Ordinal.ofFin {leap : Bool} (data : Fin (if leap = true then 61 else 60)) : Ordinal leap

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

@[inline]

def Std.Time.Second.Ordinal.toOffset {leap : Bool} (ordinal : Ordinal leap) : Offset

Converts an Ordinal to an Second.Offset.