source
inductive Std.Time.Weekday :
Type

Defines the enumeration for days of the week. Each variant corresponds to a day of the week.

- monday : Weekday

  Monday.

- tuesday : Weekday

  Tuesday.

- wednesday : Weekday

  Wednesday.

- thursday : Weekday

  Thursday.

- friday : Weekday

  Friday.

- saturday : Weekday

  Saturday.

- sunday : Weekday

  Sunday.

Instances For

source
instance Std.Time.instReprWeekday :
Repr Weekday
Equations

- Std.Time.instReprWeekday = { reprPrec := Std.Time.instReprWeekday.repr }

source
def Std.Time.instReprWeekday.repr :
Weekday → Nat → Std.Format
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

source
instance Std.Time.instInhabitedWeekday :
Inhabited Weekday
Equations

- Std.Time.instInhabitedWeekday = { default := Std.Time.instInhabitedWeekday.default }

source
def Std.Time.instInhabitedWeekday.default :
Weekday
Equations

- Std.Time.instInhabitedWeekday.default = Std.Time.Weekday.monday

Instances For

source
instance Std.Time.instDecidableEqWeekday :
DecidableEq Weekday
Equations

- Std.Time.instDecidableEqWeekday x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
def Std.Time.Weekday.Ordinal :
Type

`Ordinal` represents a bounded value for weekdays, which ranges between 1 and 7.

Equations

- Std.Time.Weekday.Ordinal = Std.Time.Internal.Bounded.LE 1 7

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

source
instance Std.Time.Weekday.instOfNatOrdinal {n : Nat} :
OfNat Ordinal n
Equations

- Std.Time.Weekday.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑6)) n)

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

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

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

- Std.Time.Weekday.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 7))

source
instance Std.Time.Weekday.instTransOrdOrdinal :
TransOrd Ordinal
source
instance Std.Time.Weekday.instLawfulEqOrdOrdinal :
LawfulEqOrd Ordinal
source
def Std.Time.Weekday.ofOrdinal :
Ordinal → Weekday

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

source
def Std.Time.Weekday.toOrdinal :
Weekday → Ordinal

Converts a `Weekday` to a `Ordinal`.

Equations

- Std.Time.Weekday.monday.toOrdinal = 1
- Std.Time.Weekday.tuesday.toOrdinal = 2
- Std.Time.Weekday.wednesday.toOrdinal = 3
- Std.Time.Weekday.thursday.toOrdinal = 4
- Std.Time.Weekday.friday.toOrdinal = 5
- Std.Time.Weekday.saturday.toOrdinal = 6
- Std.Time.Weekday.sunday.toOrdinal = 7

Instances For

source
instance Std.Time.Weekday.instOrd :
Ord Weekday
Equations

- Std.Time.Weekday.instOrd = { compare := compareOn Std.Time.Weekday.toOrdinal }

source
instance Std.Time.Weekday.instTransOrd :
TransOrd Weekday
source
theorem Std.Time.Weekday.toOrdinal.inj {a b : Weekday} (h : a.toOrdinal = b.toOrdinal) :
a = b
source
instance Std.Time.Weekday.instLawfulEqOrd :
LawfulEqOrd Weekday
source
def Std.Time.Weekday.toNat :
Weekday → Nat

Converts a `Weekday` to a `Nat`.

Equations

- Std.Time.Weekday.monday.toNat = 1
- Std.Time.Weekday.tuesday.toNat = 2
- Std.Time.Weekday.wednesday.toNat = 3
- Std.Time.Weekday.thursday.toNat = 4
- Std.Time.Weekday.friday.toNat = 5
- Std.Time.Weekday.saturday.toNat = 6
- Std.Time.Weekday.sunday.toNat = 7

Instances For

source
def Std.Time.Weekday.ofNat? :
Nat → Option Weekday

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

source
@[inline]
def Std.Time.Weekday.ofNat! (n : Nat) :
Weekday

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!" 139 12 "invalid weekday"

Instances For

source
def Std.Time.Weekday.next :
Weekday → Weekday

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

source
def Std.Time.Weekday.isWeekend :
Weekday → Bool

Check if it's a weekend.

Equations

- Std.Time.Weekday.saturday.isWeekend = true
- Std.Time.Weekday.sunday.isWeekend = true
- x✝.isWeekend = false

Instances For