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.instOrdinalRepr : Repr Std.Time.Week.Ordinal

Equations

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

instance Std.Time.Week.instOrdinalBEq : BEq Std.Time.Week.Ordinal

Equations

• Std.Time.Week.instOrdinalBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Week.instOrdinalLE : LE Std.Time.Week.Ordinal

Equations

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

instance Std.Time.Week.instOrdinalLT : LT Std.Time.Week.Ordinal

Equations

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

instance Std.Time.Week.instOfNatOrdinal {n : Nat} : OfNat Std.Time.Week.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 : Std.Time.Week.Ordinal} : Decidable (x ≤ y)

Equations

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

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

Equations

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

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

Equations

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

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.instOffsetRepr : Repr Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetBEq : BEq Std.Time.Week.Offset

Equations

• Std.Time.Week.instOffsetBEq = Std.Time.Internal.instBEqUnitVal

instance Std.Time.Week.instOffsetInhabited : Inhabited Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetAdd : Add Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetSub : Sub Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetNeg : Neg Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetLE : LE Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetLT : LT Std.Time.Week.Offset

Equations

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

instance Std.Time.Week.instOffsetToString : ToString Std.Time.Week.Offset

Equations

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

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

Equations

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

@[inline]

def Std.Time.Week.Ordinal.ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 53) : Std.Time.Week.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.instOfMonthRepr : Repr Std.Time.Week.Ordinal.OfMonth

Equations

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

@[inline]

def Std.Time.Week.Ordinal.ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 53 := by decide) : Std.Time.Week.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) : Std.Time.Week.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 : Std.Time.Week.Ordinal) : Std.Time.Week.Offset

Converts an Ordinal to an Offset.

Equations

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

@[inline]

def Std.Time.Week.Offset.ofNat (data : Nat) : Std.Time.Week.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) : Std.Time.Week.Offset

Creates an Offset from an integer.

Equations

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

@[inline]

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

Convert Week.Offset into Millisecond.Offset.

Equations

• weeks.toMilliseconds = Std.Time.Internal.UnitVal.mul weeks 604800000

@[inline]

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

Convert Millisecond.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofMilliseconds millis = Std.Time.Internal.UnitVal.ediv millis 604800000

@[inline]

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

Convert Week.Offset into Nanosecond.Offset.

Equations

• weeks.toNanoseconds = Std.Time.Internal.UnitVal.mul weeks 604800000000000

@[inline]

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

Convert Nanosecond.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofNanoseconds nanos = Std.Time.Internal.UnitVal.ediv nanos 604800000000000

@[inline]

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

Convert Week.Offset into Second.Offset.

Equations

• weeks.toSeconds = Std.Time.Internal.UnitVal.mul weeks 604800

@[inline]

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

Convert Second.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofSeconds secs = Std.Time.Internal.UnitVal.ediv secs 604800

@[inline]

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

Convert Week.Offset into Minute.Offset.

Equations

• weeks.toMinutes = Std.Time.Internal.UnitVal.mul weeks 10080

@[inline]

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

Convert Minute.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofMinutes minutes = Std.Time.Internal.UnitVal.ediv minutes 10080

@[inline]

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

Convert Week.Offset into Hour.Offset.

Equations

• weeks.toHours = Std.Time.Internal.UnitVal.mul weeks 168

@[inline]

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

Convert Hour.Offset into Week.Offset.

Equations

• Std.Time.Week.Offset.ofHours hours = Std.Time.Internal.UnitVal.ediv hours 168

@[inline]

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

Convert Week.Offset into Day.Offset.

Equations

• weeks.toDays = Std.Time.Internal.UnitVal.mul weeks 7

@[inline]

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

Convert Day.Offset into Week.Offset.

Equations

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