IotaTime.Calendar.Gregorian

Definitions

data Gregorian : Type

  The Gregorian calendar, supported from October 15, 1582 onward.

Totality: total
Visibility: public export
Constructor: 

GregorianCalendar : Gregorian

Hint: 

Calendar Gregorian

data Month : Type

Totality: total
Visibility: public export
Constructors:

January : Month

February : Month

March : Month

April : Month

May : Month

June : Month

July : Month

August : Month

September : Month

October : Month

November : Month

December : Month

Hints:

Eq Month

Ord Month

Show Month

monthNumber : Month -> Integer

Totality: total
Visibility: public export

record GregorianDate : Type

Totality: total
Visibility: export
Constructor: 

MkGregorianDate : (daysSinceEpoch : Integer) -> (0 _ : So (daysSinceEpoch >= -152444)) -> GregorianDate

Projections:

.daysSinceEpoch : GregorianDate -> Integer

0 .validDays : ({rec:0} : GregorianDate) -> So (daysSinceEpoch {rec:0} >= -152444)

Hints:

ApplyPeriod GregorianDate

CalendarNavigation GregorianDate

CalendarValue GregorianDate

Eq GregorianDate

HasCalendar GregorianDate

HasCalendarBridge GregorianDate

Ord GregorianDate

PeriodTarget GregorianDate

Show GregorianDate

isLeapYear : Year -> Bool

  Whether a Gregorian year contains February 29.

Totality: total
Visibility: public export

maxDaysInMonth : Month -> Year -> DayOfMonth

Totality: total
Visibility: public export

isValidDate : DayOfMonth -> Month -> Year -> Bool

Totality: total
Visibility: public export

epochDay : Integer

  The Gregorian calendar epoch day relative to March 1, 2000.

Totality: total
Visibility: public export

calendarDate : (valueDay : DayOfMonth) -> (valueMonth : Month) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate Gregorian

  Construct a Gregorian date whose validity is known statically.
  Use `refineDate` for values learned at runtime.

Totality: total
Visibility: public export

data GregorianDateError : Type

  Failures produced while refining untrusted Gregorian date data.

Totality: total
Visibility: public export
Constructors:

InvalidGregorianDate : DayOfMonth -> Month -> Year -> GregorianDateError

InvalidGregorianDayCount : Integer -> GregorianDateError

InvalidGregorianNthDay : DayNth -> DayOfWeek -> Month -> Year -> GregorianDateError

InvalidGregorianWeekDate : WeekNumber -> DayOfWeek -> Year -> GregorianDateError

refineDate : DayOfMonth -> Month -> Year -> Either GregorianDateError (CalendarDate Gregorian)

  Validate runtime day, month, and year components as a Gregorian date.

Totality: total
Visibility: public export

fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate Gregorian

  Construct a Gregorian date from a statically valid day count relative to
  March 1, 2000.

Totality: total
Visibility: public export

refineDays : Integer -> Either GregorianDateError (CalendarDate Gregorian)

  Validate a runtime day count relative to March 1, 2000.

Totality: total
Visibility: public export

isValidNthDay : DayNth -> DayOfWeek -> Month -> Year -> Bool

Totality: total
Visibility: public export

fromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : Month) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> CalendarDate Gregorian

  Construct the nth requested weekday in a Gregorian month under static
  validity evidence.

Totality: total
Visibility: public export

refineNthDay : DayNth -> DayOfWeek -> Month -> Year -> Either GregorianDateError (CalendarDate Gregorian)

  Validate an nth-weekday request for a Gregorian month.

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

  Construct a Gregorian Sunday-based week date under static validity evidence.

Totality: total
Visibility: public export

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

  Validate a runtime Gregorian Sunday-based week date.

Totality: total
Visibility: public export