def Std.Time.Week.Ordinal : Type

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

instance Std.Time.Week.instOrdinalRepr : Repr Ordinal

instance Std.Time.Week.instOrdinalDecidableEq : DecidableEq Ordinal

instance Std.Time.Week.instOrdinalLE : LE Ordinal

instance Std.Time.Week.instOrdinalLT : LT Ordinal

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

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

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

instance Std.Time.Week.instInhabitedOrdinal : Inhabited Ordinal

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.

instance Std.Time.Week.instOffsetRepr : Repr Offset

instance Std.Time.Week.instOffsetDecidableEq : DecidableEq Offset

instance Std.Time.Week.instOffsetInhabited : Inhabited Offset

instance Std.Time.Week.instOffsetAdd : Add Offset

instance Std.Time.Week.instOffsetSub : Sub Offset

instance Std.Time.Week.instOffsetNeg : Neg Offset

instance Std.Time.Week.instOffsetLE : LE Offset

instance Std.Time.Week.instOffsetLT : LT Offset

instance Std.Time.Week.instOffsetToString : ToString Offset

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

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

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

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.

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

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

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

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

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.