structure Time.CalendarDiffDays : Type

• months : Int
• days : Int

instance Time.instReprCalendarDiffDays : Repr Time.CalendarDiffDays

Equations

• Time.instReprCalendarDiffDays = { reprPrec := Time.reprCalendarDiffDays✝ }

instance Time.instBEqCalendarDiffDays : BEq Time.CalendarDiffDays

Equations

• Time.instBEqCalendarDiffDays = { beq := Time.beqCalendarDiffDays✝ }

instance Time.instInhabitedCalendarDiffDays : Inhabited Time.CalendarDiffDays

Equations

• Time.instInhabitedCalendarDiffDays = { default := { months := 0, days := 0 } }

def Time.calendarDay : Time.CalendarDiffDays

Equations

• Time.calendarDay = { months := 0, days := 1 }

def Time.calendarWeek : Time.CalendarDiffDays

Equations

• Time.calendarWeek = { months := 0, days := 7 }

def Time.calendarMonth : Time.CalendarDiffDays

Equations

• Time.calendarMonth = { months := 1, days := 0 }

def Time.calendarYear : Time.CalendarDiffDays

Equations

• Time.calendarYear = { months := 12, days := 0 }