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.

instance Std.Time.instReprWeekday : Repr Weekday

Equations

• Std.Time.instReprWeekday = { reprPrec := Std.Time.reprWeekday✝ }

instance Std.Time.instInhabitedWeekday : Inhabited Weekday

Equations

• Std.Time.instInhabitedWeekday = { default := Std.Time.Weekday.monday }

instance Std.Time.instDecidableEqWeekday : DecidableEq Weekday

Equations

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

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

instance Std.Time.Weekday.instReprOrdinal : Repr Ordinal

Equations

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

instance Std.Time.Weekday.instDecidableEqOrdinal : DecidableEq Ordinal

Equations

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

instance Std.Time.Weekday.instLTOrdinal : LT Ordinal

Equations

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

instance Std.Time.Weekday.instLEOrdinal : LE Ordinal

Equations

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

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

Equations

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

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

Equations

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

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)

instance Std.Time.Weekday.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

instance Std.Time.Weekday.instOrdOrdinal : Ord Ordinal

Equations

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

instance Std.Time.Weekday.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Weekday.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

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

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

instance Std.Time.Weekday.instOrd : Ord Weekday

Equations

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

instance Std.Time.Weekday.instTransOrd : TransOrd Weekday

theorem Std.Time.Weekday.toOrdinal.inj {a b : Weekday} (h : a.toOrdinal = b.toOrdinal) : a = b

instance Std.Time.Weekday.instLawfulEqOrd : LawfulEqOrd Weekday

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

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

@[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!" 141 12 "invalid weekday"

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

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