def Std.Time.Week.Offset : Type

Offset represents an offset in weeks.

@[instance_reducible]

instance Std.Time.Week.instReprOffset : Repr Offset

@[instance_reducible]

instance Std.Time.Week.instDecidableEqOffset : DecidableEq Offset

@[instance_reducible]

instance Std.Time.Week.instInhabitedOffset : Inhabited Offset

@[instance_reducible]

instance Std.Time.Week.instAddOffset : Add Offset

@[instance_reducible]

instance Std.Time.Week.instSubOffset : Sub Offset

@[instance_reducible]

instance Std.Time.Week.instNegOffset : Neg Offset

@[instance_reducible]

instance Std.Time.Week.instLEOffset : LE Offset

@[instance_reducible]

instance Std.Time.Week.instLTOffset : LT Offset

@[instance_reducible]

instance Std.Time.Week.instToStringOffset : ToString Offset

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance Std.Time.Week.instOrdOffset : Ord Offset

instance Std.Time.Week.instTransOrdOffset : TransOrd Offset

instance Std.Time.Week.instLawfulEqOrdOffset : LawfulEqOrd Offset

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

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

@[instance_reducible]

instance Std.Time.Week.OfYear.instReprOrdinal : Repr Ordinal

@[instance_reducible]

instance Std.Time.Week.OfYear.instDecidableEqOrdinal : DecidableEq Ordinal

@[instance_reducible]

instance Std.Time.Week.OfYear.instLEOrdinal : LE Ordinal

@[instance_reducible]

instance Std.Time.Week.OfYear.instLTOrdinal : LT Ordinal

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance Std.Time.Week.OfYear.instInhabitedOrdinal : Inhabited Ordinal

@[instance_reducible]

instance Std.Time.Week.OfYear.instOrdOrdinal : Ord Ordinal

instance Std.Time.Week.OfYear.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Week.OfYear.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

@[inline]

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

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

@[inline]

def Std.Time.Week.OfYear.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.OfYear.Ordinal.ofFin (data : Fin 54) : Ordinal

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

@[inline]

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

Converts an Ordinal to an Offset.

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

Ordinal represents the aligned week number within a month, ranging between 1 and 5. Aligned weeks are fixed 7-day slots counted from day 1 of the month: days 1-7 are week 1, days 8-14 are week 2, and so on, independent of which weekday starts the month.

@[instance_reducible]

instance Std.Time.Week.Aligned.instReprOrdinal : Repr Ordinal

@[instance_reducible]

instance Std.Time.Week.Aligned.instDecidableEqOrdinal : DecidableEq Ordinal

@[instance_reducible]

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

@[instance_reducible]

instance Std.Time.Week.Aligned.instInhabitedOrdinal : Inhabited Ordinal

@[instance_reducible]

instance Std.Time.Week.Aligned.instOrdOrdinal : Ord Ordinal

instance Std.Time.Week.Aligned.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Week.Aligned.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Week.Ordinal : Type

Ordinal represents the number of weeks within a month, ranging between 1 and 6.

@[instance_reducible]

instance Std.Time.Week.instReprOrdinal : Repr Ordinal

@[instance_reducible]

instance Std.Time.Week.instDecidableEqOrdinal : DecidableEq Ordinal

@[instance_reducible]

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

@[instance_reducible]

instance Std.Time.Week.instInhabitedOrdinal : Inhabited Ordinal

@[instance_reducible]

instance Std.Time.Week.instOrdOrdinal : Ord Ordinal

instance Std.Time.Week.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Week.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

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