inductive Time.FirstWeekType : Type

FirstWeekType

• FirstWholeWeek - first week is the first whole week of the year
• FirstMostWeek - first week is the first week with four days in the year

• FirstWholeWeek: Time.FirstWeekType
• FirstMostWeek: Time.FirstWeekType

instance Time.instReprFirstWeekType : Repr Time.FirstWeekType

Equations

• Time.instReprFirstWeekType = { reprPrec := Time.reprFirstWeekType✝ }

instance Time.instBEqFirstWeekType : BEq Time.FirstWeekType

Equations

• Time.instBEqFirstWeekType = { beq := Time.beqFirstWeekType✝ }

def Time.dayOfWeekDiff (a b : Time.DayOfWeek) : Int

The number of days from b to the next a.

Equations

• Time.dayOfWeekDiff a b = (a.fromDayOfWeek - b.fromDayOfWeek).emod 7

theorem Time.dayOfWeekDiff_range (a b : Time.DayOfWeek) : 0 ≤ Time.dayOfWeekDiff a b ∧ Time.dayOfWeekDiff a b ≤ 6

dayOfWeekDiff a b = a - b in range 0 to 6.

def Time.firstDayOfWeekOnAfter (dw : Time.DayOfWeek) (d : Time.Day) : Time.Day

The first day-of-week on or after some day

Equations

• Time.firstDayOfWeekOnAfter dw d = Time.Day.addDays (Time.dayOfWeekDiff dw (Time.DayOfWeek.dayOfWeek d)) d

def Time.firstDayOfWeekCalendar (wt : Time.FirstWeekType) (dow : Time.DayOfWeek) (year : Int) : Time.Day

Equations

• Time.firstDayOfWeekCalendar Time.FirstWeekType.FirstWholeWeek dow year = Time.firstDayOfWeekOnAfter dow (Time.fromOrdinalDate (Time.firstDayOfYearDate year))
• Time.firstDayOfWeekCalendar Time.FirstWeekType.FirstMostWeek dow year = Time.firstDayOfWeekOnAfter dow (Time.Day.addDays (-3) (Time.fromOrdinalDate (Time.firstDayOfYearDate year)))

def Time.toWeekCalendar (wt : Time.FirstWeekType) (ws : Time.DayOfWeek) (d : Time.Day) : Int × Int × Time.DayOfWeek

Convert to the given kind of "week calendar". Note that the year number matches the weeks, and so is not always the same as the Gregorian year number.

Equations

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

def Time.fromWeekCalendar (wt : Time.FirstWeekType) (ws : Time.DayOfWeek) (y wy : Int) (dw : Time.DayOfWeek) : Time.Day

Convert from the given kind of "week calendar". ws is the first day of each week. Invalid week and day values will be clipped to the correct range.

Equations

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

def Time.fromWeekCalendarValid (wt : Time.FirstWeekType) (ws : Time.DayOfWeek) (y wy : Int) (dw : Time.DayOfWeek) : Option Time.Day

Equations

• Time.fromWeekCalendarValid wt ws y wy dw = if (Time.toWeekCalendar wt ws (Time.fromWeekCalendar wt ws y wy dw) == (y, wy, dw)) = true then some (Time.fromWeekCalendar wt ws y wy dw) else none

def Time.fromWeekDate (y wy dw : Int) : Time.Day

Convert from ISO 8601 Week Date format.

• First argument is year,
• second week number (1-52 or 53),
• third day of week (1 for Monday to 7 for Sunday).

Invalid week and day values will be clipped to the correct range.

Equations

• Time.fromWeekDate y wy dw = Time.fromWeekCalendar Time.FirstWeekType.FirstMostWeek Time.DayOfWeek.Monday y wy (Time.DayOfWeek.toDayOfWeek dw.toNat)

def Time.fromWeekDateValid (y wy dwr : Int) : Option Time.Day

Convert from ISO 8601 Week Date format.

• First argument is year,
• second week number (1-52 or 53),
• third day of week (1 for Monday to 7 for Sunday).

Invalid week and day values will be clipped to the correct range.

Equations

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