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

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

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 : Int) (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 : Int) (wy : Int) (dw : Time.DayOfWeek) : Option Time.Day

Equations

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

def Time.fromWeekDate (y : Int) (wy : Int) (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 : Int) (wy : Int) (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.