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.

Equations

• Std.Time.Second.Ordinal leap = Std.Time.Internal.Bounded.LE 0 (Int.ofNat (if leap = true then 60 else 59))

instance Std.Time.Second.instBEqOrdinal {leap : Bool} : BEq (Std.Time.Second.Ordinal leap)

Equations

• Std.Time.Second.instBEqOrdinal = { beq := fun (x y : Std.Time.Second.Ordinal leap) => x.val == y.val }

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

Equations

• Std.Time.Second.instLEOrdinal = { le := fun (x y : Std.Time.Second.Ordinal leap) => x.val ≤ y.val }

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

Equations

• Std.Time.Second.instLTOrdinal = { lt := fun (x y : Std.Time.Second.Ordinal leap) => x.val < y.val }

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

Equations

• Std.Time.Second.instReprOrdinal = { reprPrec := fun (r : Std.Time.Second.Ordinal l) => reprPrec r.val }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

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

def Std.Time.Second.Offset : Type

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

Equations

• Std.Time.Second.Offset = Std.Time.Internal.UnitVal 1

instance Std.Time.Second.instOffsetRepr : Repr Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetBEq : BEq Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetInhabited : Inhabited Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetAdd : Add Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetSub : Sub Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetNeg : Neg Std.Time.Second.Offset

Equations

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

instance Std.Time.Second.instOffsetLE : LE Std.Time.Second.Offset

Equations

• Std.Time.Second.instOffsetLE = Std.Time.Internal.UnitVal.instLE

instance Std.Time.Second.instOffsetLT : LT Std.Time.Second.Offset

Equations

• Std.Time.Second.instOffsetLT = Std.Time.Internal.UnitVal.instLT

instance Std.Time.Second.instOffsetToString : ToString Std.Time.Second.Offset

Equations

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

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

Equations

• Std.Time.Second.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }

@[inline]

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

Creates an Second.Offset from a natural number.

Equations

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

@[inline]

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

Creates an Second.Offset from an integer.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• Std.Time.Second.Ordinal.ofFin data_2 = Std.Time.Internal.Bounded.LE.ofFin data_2
• Std.Time.Second.Ordinal.ofFin data_2 = Std.Time.Internal.Bounded.LE.ofFin data_2

@[inline]

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

Converts an Ordinal to an Second.Offset.

Equations

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