inductive Time.DayOfWeek : Type

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

instance Time.instReprDayOfWeek : Repr DayOfWeek

Equations

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

instance Time.instBEqDayOfWeek : BEq DayOfWeek

Equations

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

def Time.DayOfWeek.fromDayOfWeek : 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) : DayOfWeek

Equations

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

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

Equations

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