Equations
- Std.Time.instReprWeekday = { reprPrec := Std.Time.instReprWeekday.repr }
Equations
- Std.Time.instReprWeekday.repr Std.Time.Weekday.monday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.monday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.tuesday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.tuesday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.wednesday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.wednesday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.thursday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.thursday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.friday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.friday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.saturday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.saturday")).group prec✝
- Std.Time.instReprWeekday.repr Std.Time.Weekday.sunday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.Weekday.sunday")).group prec✝
Instances For
Equations
Instances For
Ordinal
represents a bounded value for weekdays, which ranges between 1 and 7.
Equations
Instances For
Equations
Equations
Equations
Equations
- Std.Time.Weekday.instInhabitedOrdinal = { default := 1 }
Equations
Converts a Ordinal
representing a day index into a corresponding Weekday
. This function is useful
for mapping numerical representations to days of the week.
Equations
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 1, ⋯⟩ = Std.Time.Weekday.monday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 2, ⋯⟩ = Std.Time.Weekday.tuesday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 3, ⋯⟩ = Std.Time.Weekday.wednesday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 4, ⋯⟩ = Std.Time.Weekday.thursday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 5, ⋯⟩ = Std.Time.Weekday.friday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 6, ⋯⟩ = Std.Time.Weekday.saturday
- Std.Time.Weekday.ofOrdinal ⟨Int.ofNat 7, ⋯⟩ = Std.Time.Weekday.sunday
Instances For
Equations
- Std.Time.Weekday.instOrd = { compare := compareOn Std.Time.Weekday.toOrdinal }
Equations
Instances For
Converts a Nat
to an Option Weekday
.
Equations
- Std.Time.Weekday.ofNat? 1 = some Std.Time.Weekday.monday
- Std.Time.Weekday.ofNat? 2 = some Std.Time.Weekday.tuesday
- Std.Time.Weekday.ofNat? 3 = some Std.Time.Weekday.wednesday
- Std.Time.Weekday.ofNat? 4 = some Std.Time.Weekday.thursday
- Std.Time.Weekday.ofNat? 5 = some Std.Time.Weekday.friday
- Std.Time.Weekday.ofNat? 6 = some Std.Time.Weekday.saturday
- Std.Time.Weekday.ofNat? 7 = some Std.Time.Weekday.sunday
- Std.Time.Weekday.ofNat? x✝ = none
Instances For
@[inline]
Converts a Nat
to a Weekday
. Panics if the value provided is invalid.
Equations
- Std.Time.Weekday.ofNat! n = match Std.Time.Weekday.ofNat? n with | some res => res | none => panicWithPosWithDecl "Std.Time.Date.Unit.Weekday" "Std.Time.Weekday.ofNat!" 140 12 "invalid weekday"
Instances For
Gets the next Weekday
.
Equations
- Std.Time.Weekday.monday.next = Std.Time.Weekday.tuesday
- Std.Time.Weekday.tuesday.next = Std.Time.Weekday.wednesday
- Std.Time.Weekday.wednesday.next = Std.Time.Weekday.thursday
- Std.Time.Weekday.thursday.next = Std.Time.Weekday.friday
- Std.Time.Weekday.friday.next = Std.Time.Weekday.saturday
- Std.Time.Weekday.saturday.next = Std.Time.Weekday.sunday
- Std.Time.Weekday.sunday.next = Std.Time.Weekday.monday
Instances For
Check if it's a weekend.