def Std.Time.Day.Ordinal : Type

Ordinal represents a bounded value for days, which ranges between 1 and 31.

instance Std.Time.Day.instOrdinalRepr : Repr Ordinal

instance Std.Time.Day.instOrdinalDecidableEq : DecidableEq Ordinal

instance Std.Time.Day.instOrdinalLE : LE Ordinal

instance Std.Time.Day.instOrdinalLT : LT Ordinal

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

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

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

instance Std.Time.Day.instInhabitedOrdinal : Inhabited Ordinal

instance Std.Time.Day.instOrdOrdinal : Ord Ordinal

instance Std.Time.Day.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Day.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Day.Offset : Type

Offset represents an offset in days. It is defined as an Int with a base unit of 86400 (the number of seconds in a day).

instance Std.Time.Day.instOffsetRepr : Repr Offset

instance Std.Time.Day.instOffsetDecidableEq : DecidableEq Offset

instance Std.Time.Day.instOffsetInhabited : Inhabited Offset

instance Std.Time.Day.instOffsetAdd : Add Offset

instance Std.Time.Day.instOffsetSub : Sub Offset

instance Std.Time.Day.instOffsetNeg : Neg Offset

instance Std.Time.Day.instOffsetLE : LE Offset

instance Std.Time.Day.instOffsetLT : LT Offset

instance Std.Time.Day.instOffsetToString : ToString Offset

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

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

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

instance Std.Time.Day.instOrdOffset : Ord Offset

instance Std.Time.Day.instTransOrdOffset : TransOrd Offset

instance Std.Time.Day.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

def Std.Time.Day.Ordinal.ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 31) : Ordinal

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

def Std.Time.Day.Ordinal.OfYear (leap : Bool) : Type

OfYear represents the day ordinal within a year, which can be bounded between 1 and 365 or 366, depending on whether it's a leap year.

instance Std.Time.Day.Ordinal.instReprOfYear {leap : Bool} : Repr (OfYear leap)

instance Std.Time.Day.Ordinal.instToStringOfYear {leap : Bool} : ToString (OfYear leap)

instance Std.Time.Day.Ordinal.instDecidableEqOfYear {leap : Bool} : DecidableEq (OfYear leap)

instance Std.Time.Day.Ordinal.instOrdOfYear {leap : Bool} : Ord (OfYear leap)

instance Std.Time.Day.Ordinal.instTransOrdOfYear {leap : Bool} : TransOrd (OfYear leap)

instance Std.Time.Day.Ordinal.instLawfulEqOrdOfYear {leap : Bool} : LawfulEqOrd (OfYear leap)

@[inline]

def Std.Time.Day.Ordinal.OfYear.ofNat {leap : Bool} (data : Nat) (h : data ≥ 1 ∧ data ≤ if leap = true then 366 else 365 := by decide) : OfYear leap

Creates an ordinal for a specific day within the year, ensuring that the provided day (data) is within the valid range for the year, which can be 1 to 365 or 366 for leap years.

instance Std.Time.Day.Ordinal.instOfNatOfYear {leap : Bool} {n : Nat} : OfNat (OfYear leap) n

instance Std.Time.Day.Ordinal.instInhabitedOfYear {leap : Bool} : Inhabited (OfYear leap)

@[inline]

def Std.Time.Day.Ordinal.ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 31 := by decide) : Ordinal

Creates an ordinal from a natural number, ensuring the number is within the valid range for days of a month (1 to 31).

@[inline]

def Std.Time.Day.Ordinal.ofFin (data : Fin 32) : Ordinal

Creates an ordinal from a Fin value, ensuring it is within the valid range for days of the month (1 to 31). If the Fin value is 0, it is converted to 1.

@[inline]

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

Converts an Ordinal to an Offset.

def Std.Time.Day.Ordinal.OfYear.toOffset {leap : Bool} (ofYear : OfYear leap) : Offset

Converts an OfYear ordinal to a Offset.

@[inline]

def Std.Time.Day.Offset.toOrdinal (off : Offset) (h : off.val ≥ 1 ∧ off.val ≤ 31) : Ordinal

Converts an Offset to an Ordinal.

@[inline]

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

Creates an Offset from a natural number.

@[inline]

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

Creates an Offset from an integer.

@[inline]

def Std.Time.Day.Offset.toNanoseconds (days : Offset) : Nanosecond.Offset

Convert Day.Offset into Nanosecond.Offset.

@[inline]

def Std.Time.Day.Offset.ofNanoseconds (ns : Nanosecond.Offset) : Offset

Convert Nanosecond.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toMilliseconds (days : Offset) : Millisecond.Offset

Convert Day.Offset into Millisecond.Offset.

@[inline]

def Std.Time.Day.Offset.ofMilliseconds (ms : Millisecond.Offset) : Offset

Convert Millisecond.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toSeconds (days : Offset) : Second.Offset

Convert Day.Offset into Second.Offset.

@[inline]

def Std.Time.Day.Offset.ofSeconds (secs : Second.Offset) : Offset

Convert Second.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toMinutes (days : Offset) : Minute.Offset

Convert Day.Offset into Minute.Offset.

@[inline]

def Std.Time.Day.Offset.ofMinutes (minutes : Minute.Offset) : Offset

Convert Minute.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toHours (days : Offset) : Hour.Offset

Convert Day.Offset into Hour.Offset.

@[inline]

def Std.Time.Day.Offset.ofHours (hours : Hour.Offset) : Offset

Convert Hour.Offset into Day.Offset.