def Std.Time.Week.Offset : Type

Offset represents an offset in weeks.

Equations

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

@[instance_reducible]

instance Std.Time.Week.instReprOffset : Repr Offset

Equations

• Std.Time.Week.instReprOffset = { reprPrec := Std.Time.Week.instReprOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.Week.instDecidableEqOffset = Std.Time.Week.instDecidableEqOffset._aux_1

@[instance_reducible]

instance Std.Time.Week.instInhabitedOffset : Inhabited Offset

Equations

• Std.Time.Week.instInhabitedOffset = { default := Std.Time.Week.instInhabitedOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instAddOffset : Add Offset

Equations

• Std.Time.Week.instAddOffset = { add := Std.Time.Week.instAddOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instSubOffset : Sub Offset

Equations

• Std.Time.Week.instSubOffset = { sub := Std.Time.Week.instSubOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instNegOffset : Neg Offset

Equations

• Std.Time.Week.instNegOffset = { neg := Std.Time.Week.instNegOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instLEOffset : LE Offset

Equations

• Std.Time.Week.instLEOffset = { le := Std.Time.Week.instLEOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instLTOffset : LT Offset

Equations

• Std.Time.Week.instLTOffset = { lt := Std.Time.Week.instLTOffset._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instToStringOffset : ToString Offset

Equations

• Std.Time.Week.instToStringOffset = { toString := Std.Time.Week.instToStringOffset._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.instDecidableLeOffset = Std.Time.Week.instDecidableLeOffset._aux_1

@[instance_reducible]

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

Equations

• Std.Time.Week.instDecidableLtOffset = Std.Time.Week.instDecidableLtOffset._aux_1

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Std.Time.Week.instOrdOffset : Ord Offset

Equations

• Std.Time.Week.instOrdOffset = { compare := Std.Time.Week.instOrdOffset._aux_1 }

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.

Equations

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

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instReprOrdinal = { reprPrec := Std.Time.Week.OfYear.instReprOrdinal._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instDecidableEqOrdinal = Std.Time.Week.OfYear.instDecidableEqOrdinal._aux_1

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instLEOrdinal = { le := Std.Time.Week.OfYear.instLEOrdinal._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instLTOrdinal = { lt := Std.Time.Week.OfYear.instLTOrdinal._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instOfNatOrdinal = { ofNat := Std.Time.Week.OfYear.instOfNatOrdinal._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instDecidableLeOrdinal = Std.Time.Week.OfYear.instDecidableLeOrdinal._aux_1

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instDecidableLtOrdinal = Std.Time.Week.OfYear.instDecidableLtOrdinal._aux_1

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Std.Time.Week.OfYear.instOrdOrdinal = { compare := Std.Time.Week.OfYear.instOrdOrdinal._aux_1 }

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.

Equations

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

Converts an Ordinal to an Offset.

Equations

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

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.

Equations

• Std.Time.Week.Aligned.Ordinal = Std.Time.Internal.Bounded.LE 1 5

@[instance_reducible]

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

Equations

• Std.Time.Week.Aligned.instReprOrdinal = { reprPrec := Std.Time.Week.Aligned.instReprOrdinal._aux_1 }

@[instance_reducible]

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

Equations

• Std.Time.Week.Aligned.instDecidableEqOrdinal = Std.Time.Week.Aligned.instDecidableEqOrdinal._aux_1

@[instance_reducible]

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

Equations

• Std.Time.Week.Aligned.instOfNatOrdinal = { ofNat := Std.Time.Week.Aligned.instOfNatOrdinal._aux_1 }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Std.Time.Week.Aligned.instOrdOrdinal = { compare := Std.Time.Week.Aligned.instOrdOrdinal._aux_1 }

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.

Equations

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

@[instance_reducible]

instance Std.Time.Week.instReprOrdinal : Repr Ordinal

Equations

• Std.Time.Week.instReprOrdinal = { reprPrec := Std.Time.Week.instReprOrdinal._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instDecidableEqOrdinal : DecidableEq Ordinal

Equations

• Std.Time.Week.instDecidableEqOrdinal = Std.Time.Week.instDecidableEqOrdinal._aux_1

@[instance_reducible]

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

Equations

• Std.Time.Week.instOfNatOrdinal = { ofNat := Std.Time.Week.instOfNatOrdinal._aux_1 }

@[instance_reducible]

instance Std.Time.Week.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

@[instance_reducible]

instance Std.Time.Week.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Week.instOrdOrdinal = { compare := Std.Time.Week.instOrdOrdinal._aux_1 }

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.

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