def Std.Time.Week.Ordinal : Type

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

Equations

• Std.Time.Week.Ordinal = Std.Time.Internal.Bounded.LE 1 53

instance Std.Time.Week.instReprOrdinal : Repr Ordinal

Equations

• Std.Time.Week.instReprOrdinal = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Week.instDecidableEqOrdinal : DecidableEq Ordinal

Equations

• Std.Time.Week.instDecidableEqOrdinal = Std.Time.Internal.Bounded.instDecidableEq

instance Std.Time.Week.instLEOrdinal : LE Ordinal

Equations

• Std.Time.Week.instLEOrdinal = Std.Time.Internal.Bounded.instLE

instance Std.Time.Week.instLTOrdinal : LT Ordinal

Equations

• Std.Time.Week.instLTOrdinal = Std.Time.Internal.Bounded.instLT

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

Equations

• Std.Time.Week.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑52)) n)

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

Equations

• Std.Time.Week.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

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

Equations

• Std.Time.Week.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

instance Std.Time.Week.instInhabitedOrdinal : Inhabited Ordinal

Equations

• Std.Time.Week.instInhabitedOrdinal = { default := 1 }

instance Std.Time.Week.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Week.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 53))

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.

Equations

• Std.Time.Week.Offset = Std.Time.Internal.UnitVal (86400 * 7)

instance Std.Time.Week.instReprOffset : Repr Offset

Equations

• Std.Time.Week.instReprOffset = Std.Time.Internal.UnitVal.instRepr

instance Std.Time.Week.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.Week.instDecidableEqOffset = Std.Time.Internal.instDecidableEqUnitVal

instance Std.Time.Week.instInhabitedOffset : Inhabited Offset

Equations

• Std.Time.Week.instInhabitedOffset = Std.Time.Internal.instInhabitedUnitVal

instance Std.Time.Week.instAddOffset : Add Offset

Equations

• Std.Time.Week.instAddOffset = Std.Time.Internal.UnitVal.instAdd

instance Std.Time.Week.instSubOffset : Sub Offset

Equations

• Std.Time.Week.instSubOffset = Std.Time.Internal.UnitVal.instSub

instance Std.Time.Week.instNegOffset : Neg Offset

Equations

• Std.Time.Week.instNegOffset = Std.Time.Internal.UnitVal.instNeg

instance Std.Time.Week.instLEOffset : LE Offset

Equations

• Std.Time.Week.instLEOffset = Std.Time.Internal.UnitVal.instLE

instance Std.Time.Week.instLTOffset : LT Offset

Equations

• Std.Time.Week.instLTOffset = Std.Time.Internal.UnitVal.instLT

instance Std.Time.Week.instToStringOffset : ToString Offset

Equations

• Std.Time.Week.instToStringOffset = Std.Time.Internal.UnitVal.instToString

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

Equations

• Std.Time.Week.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

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

Equations

• Std.Time.Week.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

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

Equations

• Std.Time.Week.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }

instance Std.Time.Week.instOrdOffset : Ord Offset

Equations

• Std.Time.Week.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal (86400 * 7)))

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.

Equations

• Std.Time.Week.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

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.

Equations

• Std.Time.Week.Ordinal.OfMonth = Std.Time.Internal.Bounded.LE 1 6

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

Equations

• Std.Time.Week.Ordinal.instReprOfMonth = Std.Time.Internal.Bounded.instRepr

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

Equations

• Std.Time.Week.Ordinal.instDecidableEqOfMonth = Std.Time.Internal.Bounded.instDecidableEq

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

Equations

• Std.Time.Week.Ordinal.instOfNatOfMonth = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑5)) n)

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

Equations

• Std.Time.Week.Ordinal.instInhabitedOfMonth = { default := 1 }

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

Equations

• Std.Time.Week.Ordinal.instOrdOfMonth = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 6))

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.

Equations

• Std.Time.Week.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat' data h

@[inline]

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

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

Equations

• Std.Time.Week.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin' data Std.Time.Week.Ordinal.ofFin._proof_1✝

@[inline]

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

Converts an Ordinal to an Offset.

Equations

• ordinal.toOffset = { val := ordinal.val }

@[inline]

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

Creates an Offset from a natural number.

Equations

• Std.Time.Week.Offset.ofNat data = { val := ↑data }

@[inline]

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

Creates an Offset from an integer.

Equations

• Std.Time.Week.Offset.ofInt data = { val := data }

@[inline]

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

Convert Week.Offset into Millisecond.Offset.

Equations

• weeks.toMilliseconds = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 604800000)

@[inline]

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

Convert Millisecond.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofMilliseconds millis = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.ofMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv millis 604800000)

@[inline]

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

Convert Week.Offset into Nanosecond.Offset.

Equations

• weeks.toNanoseconds = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toNanoseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 604800000000000)

@[inline]

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

Convert Nanosecond.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofNanoseconds nanos = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.ofNanoseconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv nanos 604800000000000)

@[inline]

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

Convert Week.Offset into Second.Offset.

Equations

• weeks.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toSeconds._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 604800)

@[inline]

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

Convert Second.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofSeconds secs = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.ofSeconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv secs 604800)

@[inline]

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

Convert Week.Offset into Minute.Offset.

Equations

• weeks.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 10080)

@[inline]

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

Convert Minute.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofMinutes minutes = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.ediv minutes 10080)

@[inline]

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

Convert Week.Offset into Hour.Offset.

Equations

• weeks.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 168)

@[inline]

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

Convert Hour.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofHours hours = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.ediv hours 168)

@[inline]

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

Convert Week.Offset into Day.Offset.

Equations

• weeks.toDays = Std.Time.Internal.UnitVal.cast Std.Time.Week.Offset.toDays._proof_1✝ (Std.Time.Internal.UnitVal.mul weeks 7)

@[inline]

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

Convert Day.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofDays days = Std.Time.Internal.UnitVal.ediv days 7