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

def Std.Time.instReprWeekday.repr : Weekday → Nat → Std.Format

instance Std.Time.instInhabitedWeekday : Inhabited Weekday

def Std.Time.instInhabitedWeekday.default : Weekday

instance Std.Time.instDecidableEqWeekday : DecidableEq Weekday

def Std.Time.Weekday.Ordinal : Type

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

instance Std.Time.Weekday.instReprOrdinal : Repr Ordinal

instance Std.Time.Weekday.instDecidableEqOrdinal : DecidableEq Ordinal

instance Std.Time.Weekday.instLTOrdinal : LT Ordinal

instance Std.Time.Weekday.instLEOrdinal : LE Ordinal

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

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

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

instance Std.Time.Weekday.instInhabitedOrdinal : Inhabited Ordinal

instance Std.Time.Weekday.instOrdOrdinal : Ord Ordinal

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.

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

Converts a Weekday to a Ordinal.

instance Std.Time.Weekday.instOrd : Ord Weekday

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.

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

Converts a Nat to an Option Weekday.

@[inline]

def Std.Time.Weekday.ofNat! (n : Nat) : Weekday

Converts a Nat to a Weekday. Panics if the value provided is invalid.

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

Gets the next Weekday.

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

Check if it's a weekend.