IotaTime.Calendar.Iso

Reexports

Definitions

daysFromCivil : Year -> Integer -> Integer -> Integer

Totality: total
Visibility: public export

weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer

Totality: total
Visibility: public export

hasFiftyThreeWeeks : Year -> Bool

  Whether an ISO week-numbering year contains week 53.

Totality: total
Visibility: public export

weeksInIsoYear : Year -> WeekNumber

  The number of ISO weeks in a year, either 52 or 53.

Totality: total
Visibility: public export

isValidIsoWeekNumber : WeekNumber -> Year -> Bool

  Whether a week number belongs to the requested ISO week-numbering year.

Totality: total
Visibility: public export

isValidArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool

  Whether an unrestricted arithmetic week coordinate resolves inside the
  supported Gregorian range.

Totality: total
Visibility: public export

isValidWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool

  Whether a standards-valid ISO week date resolves inside the supported
  Gregorian range.

Totality: total
Visibility: public export

arithmeticFromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticWeekDate week target valueYear)} -> CalendarDate Gregorian

  Construct an unrestricted arithmetic ISO week coordinate. Unlike
  `fromWeekDate`, this operation deliberately permits week zero and values
  beyond the requested ISO year.

Totality: total
Visibility: public export

fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate Gregorian

  Construct a Gregorian date using ISO-8601 week numbering. Weeks start on
  Monday, week 1 contains January 4, and the week must belong to the requested
  ISO week-numbering year.

Totality: total
Visibility: public export

data IsoWeekDateError : Type

Totality: total
Visibility: public export
Constructors:

InvalidIsoWeekDate : WeekNumber -> DayOfWeek -> Year -> IsoWeekDateError

ArithmeticIsoWeekDateOutOfRange : WeekNumber -> DayOfWeek -> Year -> IsoWeekDateError

refineWeekDate : WeekNumber -> DayOfWeek -> Year -> Either IsoWeekDateError (CalendarDate Gregorian)

  Validate an ISO week date learned at runtime.

Totality: total
Visibility: public export

refineArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year -> Either IsoWeekDateError (CalendarDate Gregorian)

  Validate an unrestricted arithmetic week coordinate learned at runtime.

Totality: total
Visibility: public export