source
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

Instances For

source
instance Std.Time.Week.instReprOrdinal :
Repr Ordinal
Equations

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

source
instance Std.Time.Week.instDecidableEqOrdinal :
DecidableEq Ordinal
Equations

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

source
instance Std.Time.Week.instLEOrdinal :
LE Ordinal
Equations

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

source
instance Std.Time.Week.instLTOrdinal :
LT Ordinal
Equations

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

source
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)

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

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

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

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

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

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

source
instance Std.Time.Week.instOrdOrdinal :
Ord Ordinal
Equations

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

source
instance Std.Time.Week.instTransOrdOrdinal :
TransOrd Ordinal
source
instance Std.Time.Week.instLawfulEqOrdOrdinal :
LawfulEqOrd Ordinal
source
def Std.Time.Week.Offset :
Type

`Offset` represents an offset in weeks.

Equations

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

Instances For

source
instance Std.Time.Week.instReprOffset :
Repr Offset
Equations

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

source
instance Std.Time.Week.instDecidableEqOffset :
DecidableEq Offset
Equations

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

source
instance Std.Time.Week.instInhabitedOffset :
Inhabited Offset
Equations

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

source
instance Std.Time.Week.instAddOffset :
Add Offset
Equations

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

source
instance Std.Time.Week.instSubOffset :
Sub Offset
Equations

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

source
instance Std.Time.Week.instNegOffset :
Neg Offset
Equations

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

source
instance Std.Time.Week.instLEOffset :
LE Offset
Equations

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

source
instance Std.Time.Week.instLTOffset :
LT Offset
Equations

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

source
instance Std.Time.Week.instToStringOffset :
ToString Offset
Equations

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

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

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

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

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

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

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

source
instance Std.Time.Week.instOrdOffset :
Ord Offset
Equations

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

source
instance Std.Time.Week.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.Week.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
@[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

Instances For

source
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

Instances For

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

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

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

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

source
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)

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

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

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

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

source
instance Std.Time.Week.Ordinal.instTransOrdOfMonth :
TransOrd OfMonth
source
instance Std.Time.Week.Ordinal.instLawfulEqOrdOfMonth :
LawfulEqOrd OfMonth
source
@[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

Instances For

source
@[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✝

Instances For

source
@[inline]
def Std.Time.Week.Ordinal.toOffset (ordinal : Ordinal) :
Offset

Converts an `Ordinal` to an `Offset`.

Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

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

Instances For