Documentation

Std.Time.Date.Unit.Weekday

inductive Std.Time.Weekday :

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

instance Std.Time.instReprWeekday :

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.instBEqWeekday :

Equations

Std.Time.instBEqWeekday = { beq := Std.Time.beqWeekday✝ }

def Std.Time.Weekday.Ordinal :

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

Std.Time.Weekday.instOfNatOrdinal

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)

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

def Std.Time.Weekday.toNat :

Weekday → Nat

Converts a Weekday to a Nat.

Equations

def Std.Time.Weekday.ofNat? :

Nat → Option Weekday

Converts a Nat to an Option Weekday.

@[inline]

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

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

def Std.Time.Weekday.isWeekend :

Weekday → Bool

Check if it's a weekend.

Equations