Std.Time.Time.Unit.Second

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

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

Instances For

source

@[implicit_reducible]

instance Std.Time.Second.instLEOrdinal {leap : Bool} :

LE (Ordinal leap)

source

@[implicit_reducible]

instance Std.Time.Second.instLTOrdinal {leap : Bool} :

LT (Ordinal leap)

source

@[implicit_reducible]

instance Std.Time.Second.instReprOrdinal {leap : Bool} :

Repr (Ordinal leap)

source

@[implicit_reducible]

instance Std.Time.Second.instToStringOrdinal {leap : Bool} :

ToString (Ordinal leap)

source

@[implicit_reducible]

instance Std.Time.Second.instOfNatOrdinal {leap : Bool} {n : Nat} :

OfNat (Ordinal leap) n

source

@[implicit_reducible]

instance Std.Time.Second.instDecidableLeOrdinal {leap : Bool} {x y : Ordinal leap} :

Decidable (x ≤ y)

source

@[implicit_reducible]

instance Std.Time.Second.instDecidableLtOrdinal {leap : Bool} {x y : Ordinal leap} :

Decidable (x < y)

source

@[implicit_reducible]

instance Std.Time.Second.instDecidableEqOrdinal {leap : Bool} :

DecidableEq (Ordinal leap)

source

@[implicit_reducible]

instance Std.Time.Second.instOrdOrdinal {leap : Bool} :

Ord (Ordinal leap)

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.

Instances For

source

@[implicit_reducible]

instance Std.Time.Second.instReprOffset :

Repr Offset

source

@[implicit_reducible]

instance Std.Time.Second.instDecidableEqOffset :

DecidableEq Offset

source

@[implicit_reducible]

instance Std.Time.Second.instInhabitedOffset :

Inhabited Offset

source

@[implicit_reducible]

instance Std.Time.Second.instAddOffset :

Add Offset

source

@[implicit_reducible]

instance Std.Time.Second.instSubOffset :

Sub Offset

source

@[implicit_reducible]

instance Std.Time.Second.instNegOffset :

Neg Offset

source

@[implicit_reducible]

instance Std.Time.Second.instLEOffset :

LE Offset

source

@[implicit_reducible]

instance Std.Time.Second.instLTOffset :

LT Offset

source

@[implicit_reducible]

instance Std.Time.Second.instToStringOffset :

ToString Offset

source

@[implicit_reducible]

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

Decidable (x ≤ y)

source

@[implicit_reducible]

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

Decidable (x < y)

source

@[implicit_reducible]

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

OfNat Offset n

source

@[implicit_reducible]

instance Std.Time.Second.instOrdOffset :

Ord Offset

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.

Instances For

source

@[inline]

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

Offset

Creates an Second.Offset from an integer.

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.

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.

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.

Instances For

source

@[inline]

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

Offset

Converts an Ordinal to an Second.Offset.

Instances For