inductive Time.DayOfWeek : Type

• Monday: Time.DayOfWeek
• Tuesday: Time.DayOfWeek
• Wednesday: Time.DayOfWeek
• Thursday: Time.DayOfWeek
• Friday: Time.DayOfWeek
• Saturday: Time.DayOfWeek
• Sunday: Time.DayOfWeek

instance Time.instReprDayOfWeek : Repr Time.DayOfWeek

Equations

• Time.instReprDayOfWeek = { reprPrec := Time.reprDayOfWeek✝ }

instance Time.instBEqDayOfWeek : BEq Time.DayOfWeek

Equations

• Time.instBEqDayOfWeek = { beq := Time.beqDayOfWeek✝ }

def Time.DayOfWeek.fromDayOfWeek : Time.DayOfWeek → Int

Equations

• One or more equations did not get rendered due to their size.

def Time.DayOfWeek.toDayOfWeek (n : Nat) : Time.DayOfWeek

Equations

• One or more equations did not get rendered due to their size.

def Time.DayOfWeek.dayOfWeek (d : Time.Day) : Time.DayOfWeek

Equations

• Time.DayOfWeek.dayOfWeek d = Time.DayOfWeek.toDayOfWeek (d.modifiedJulianDay.toNat + 3)