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

• Time.DayOfWeek.Monday.fromDayOfWeek = 1
• Time.DayOfWeek.Tuesday.fromDayOfWeek = 2
• Time.DayOfWeek.Wednesday.fromDayOfWeek = 3
• Time.DayOfWeek.Thursday.fromDayOfWeek = 4
• Time.DayOfWeek.Friday.fromDayOfWeek = 5
• Time.DayOfWeek.Saturday.fromDayOfWeek = 6
• Time.DayOfWeek.Sunday.fromDayOfWeek = 7

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)