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

Instances For

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

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

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

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

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

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

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

- Std.Time.Second.instToStringOrdinal = { toString := fun (r : Std.Time.Second.Ordinal leap) => toString r.val }

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

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

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

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

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

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

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

- Std.Time.Second.instDecidableEqOrdinal = inferInstanceAs (DecidableEq (Std.Time.Internal.Bounded.LE 0 (Int.ofNat (if leap = true then 60 else 59))))

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

- Std.Time.Second.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 0 (Int.ofNat (if leap = true then 60 else 59))))

source
instance Std.Time.Second.instTransOrdOrdinal {leap : Bool} :
TransOrd (Ordinal leap)
source
instance Std.Time.Second.instLawfulEqOrdOrdinal {leap : Bool} :
LawfulEqOrd (Ordinal leap)
source
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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

- Std.Time.Second.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal 1))

source
instance Std.Time.Second.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.Second.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
@[inline]
def Std.Time.Second.Offset.ofNat (data : Nat) :
Offset

Creates an `Second.Offset` from a natural number.

Equations

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

Instances For

source
@[inline]
def Std.Time.Second.Offset.ofInt (data : Int) :
Offset

Creates an `Second.Offset` from an integer.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

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

Instances For

source
@[inline]
def Std.Time.Second.Ordinal.toOffset {leap : Bool} (ordinal : Ordinal leap) :
Offset

Converts an `Ordinal` to an `Second.Offset`.

Equations

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

Instances For