def Std.Time.Week.Ordinal : Type

Ordinal represents a bounded value for weeks, which ranges between 1 and 53.

@[implicit_reducible]

instance Std.Time.Week.instReprOrdinal : Repr Ordinal

@[implicit_reducible]

instance Std.Time.Week.instDecidableEqOrdinal : DecidableEq Ordinal

@[implicit_reducible]

instance Std.Time.Week.instLEOrdinal : LE Ordinal

@[implicit_reducible]

instance Std.Time.Week.instLTOrdinal : LT Ordinal

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Std.Time.Week.instInhabitedOrdinal : Inhabited Ordinal

@[implicit_reducible]

instance Std.Time.Week.instOrdOrdinal : Ord Ordinal

instance Std.Time.Week.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Week.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Week.Offset : Type

Offset represents an offset in weeks.

@[implicit_reducible]

instance Std.Time.Week.instReprOffset : Repr Offset

@[implicit_reducible]

instance Std.Time.Week.instDecidableEqOffset : DecidableEq Offset

@[implicit_reducible]

instance Std.Time.Week.instInhabitedOffset : Inhabited Offset

@[implicit_reducible]

instance Std.Time.Week.instAddOffset : Add Offset

@[implicit_reducible]

instance Std.Time.Week.instSubOffset : Sub Offset

@[implicit_reducible]

instance Std.Time.Week.instNegOffset : Neg Offset

@[implicit_reducible]

instance Std.Time.Week.instLEOffset : LE Offset

@[implicit_reducible]

instance Std.Time.Week.instLTOffset : LT Offset

@[implicit_reducible]

instance Std.Time.Week.instToStringOffset : ToString Offset

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Std.Time.Week.instOrdOffset : Ord Offset

instance Std.Time.Week.instTransOrdOffset : TransOrd Offset

instance Std.Time.Week.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

def Std.Time.Week.Ordinal.ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 53) : Ordinal

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

def Std.Time.Week.Ordinal.OfMonth : Type

OfMonth represents the number of weeks within a month. It ensures that the week is within the correct bounds—either 1 to 6, representing the possible weeks in a month.

@[implicit_reducible]

instance Std.Time.Week.Ordinal.instReprOfMonth : Repr OfMonth

@[implicit_reducible]

instance Std.Time.Week.Ordinal.instDecidableEqOfMonth : DecidableEq OfMonth

@[implicit_reducible]

instance Std.Time.Week.Ordinal.instOfNatOfMonth {n : Nat} : OfNat OfMonth n

@[implicit_reducible]

instance Std.Time.Week.Ordinal.instInhabitedOfMonth : Inhabited OfMonth

@[implicit_reducible]

instance Std.Time.Week.Ordinal.instOrdOfMonth : Ord OfMonth

instance Std.Time.Week.Ordinal.instTransOrdOfMonth : TransOrd OfMonth

instance Std.Time.Week.Ordinal.instLawfulEqOrdOfMonth : LawfulEqOrd OfMonth

@[inline]

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

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

@[inline]

def Std.Time.Week.Ordinal.ofFin (data : Fin 54) : Ordinal

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

@[inline]

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

Converts an Ordinal to an Offset.

@[inline]

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

Creates an Offset from a natural number.

@[inline]

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

Creates an Offset from an integer.

@[inline]

def Std.Time.Week.Offset.toMilliseconds (weeks : Offset) : Millisecond.Offset

Convert Week.Offset into Millisecond.Offset.

@[inline]

def Std.Time.Week.Offset.ofMilliseconds (millis : Millisecond.Offset) : Offset

Convert Millisecond.Offset into Week.Offset.

@[inline]

def Std.Time.Week.Offset.toNanoseconds (weeks : Offset) : Nanosecond.Offset

Convert Week.Offset into Nanosecond.Offset.

@[inline]

def Std.Time.Week.Offset.ofNanoseconds (nanos : Nanosecond.Offset) : Offset

Convert Nanosecond.Offset into Week.Offset.

@[inline]

def Std.Time.Week.Offset.toSeconds (weeks : Offset) : Second.Offset

Convert Week.Offset into Second.Offset.

@[inline]

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

Convert Second.Offset into Week.Offset.

@[inline]

def Std.Time.Week.Offset.toMinutes (weeks : Offset) : Minute.Offset

Convert Week.Offset into Minute.Offset.

@[inline]

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

Convert Minute.Offset into Week.Offset.

@[inline]

def Std.Time.Week.Offset.toHours (weeks : Offset) : Hour.Offset

Convert Week.Offset into Hour.Offset.

@[inline]

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

Convert Hour.Offset into Week.Offset.

@[inline]

def Std.Time.Week.Offset.toDays (weeks : Offset) : Day.Offset

Convert Week.Offset into Day.Offset.

@[inline]

def Std.Time.Week.Offset.ofDays (days : Day.Offset) : Offset

Convert Day.Offset into Week.Offset.