Idris2Doc : IotaTime.Calendar.Coptic

IotaTime.Calendar.Coptic

(source)
Definitions
data Coptic : Type
  The 13-month Coptic calendar, supported from 1 Thout 1.

  Totality: total
  Visibility: public export
  Constructor: 
CopticCalendar : Coptic

  Hint: 
Calendar Coptic
data CopticMonth : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Thout : CopticMonth
  
Paopi : CopticMonth
  
Hathor : CopticMonth
  
Koiak : CopticMonth
  
Tobi : CopticMonth
  
Meshir : CopticMonth
  
Paremhat : CopticMonth
  
Paremoude : CopticMonth
  
Pashons : CopticMonth
  
Paoni : CopticMonth
  
Epip : CopticMonth
  
Mesori : CopticMonth
  
PiKogiEnavot : CopticMonth

  Hints:
  
Eq CopticMonth
  
Ord CopticMonth
  
Show CopticMonth
monthNumber : CopticMonth -> Integer
  Totality: total
  Visibility: public export
record CopticDate : Type
  Totality: total
  Visibility: export
  Constructor: 
MkCopticDate : (daysSinceEpoch : Integer) -> (0 _ : So (daysSinceEpoch >= -626575)) -> CopticDate

  Projections:
  
.daysSinceEpoch : CopticDate -> Integer
  
0 .validDays : ({rec:0} : CopticDate) -> So (daysSinceEpoch {rec:0} >= -626575)

  Hints:
  
ApplyPeriod CopticDate
  
CalendarNavigation CopticDate
  
CalendarValue CopticDate
  
Eq CopticDate
  
HasCalendar CopticDate
  
HasCalendarBridge CopticDate
  
Ord CopticDate
  
PeriodTarget CopticDate
  
Show CopticDate
epochDay : Integer
  The Coptic calendar epoch day relative to March 1, 2000 Gregorian.

  Totality: total
  Visibility: public export
isLeapYear : Year -> Bool
  Whether a Coptic year has a sixth epagomenal day.

  Totality: total
  Visibility: public export
maxDaysInMonth : CopticMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidDate : DayOfMonth -> CopticMonth -> Year -> Bool
  Totality: total
  Visibility: public export
calendarDate : (valueDay : DayOfMonth) -> (valueMonth : CopticMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate Coptic
  Construct a statically validated Coptic date.

  Totality: total
  Visibility: public export
data CopticDateError : Type
  Failures produced while refining untrusted Coptic date data.

  Totality: total
  Visibility: public export
  Constructors:
  
InvalidCopticDate : DayOfMonth -> CopticMonth -> Year -> CopticDateError
  
InvalidCopticDayCount : Integer -> CopticDateError
  
InvalidCopticNthDay : DayNth -> DayOfWeek -> CopticMonth -> Year -> CopticDateError
  
InvalidCopticWeekDate : WeekNumber -> DayOfWeek -> Year -> CopticDateError
refineDate : DayOfMonth -> CopticMonth -> Year -> Either CopticDateError (CalendarDate Coptic)
  Validate runtime day, month, and year components as a Coptic date.

  Totality: total
  Visibility: public export
fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate Coptic
  Construct a Coptic date from a statically valid calendar-relative day count.

  Totality: total
  Visibility: public export
refineDays : Integer -> Either CopticDateError (CalendarDate Coptic)
  Validate a runtime Coptic day count.

  Totality: total
  Visibility: public export
isValidNthDay : DayNth -> DayOfWeek -> CopticMonth -> Year -> Bool
  Totality: total
  Visibility: public export
nthDayOfMonth : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : CopticMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> DayOfMonth
  Return the requested weekday occurrence under static validity evidence.

  Totality: total
  Visibility: public export
fromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : CopticMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> CalendarDate Coptic
  Construct the nth requested weekday in a Coptic month.

  Totality: total
  Visibility: public export
refineNthDay : DayNth -> DayOfWeek -> CopticMonth -> Year -> Either CopticDateError (CalendarDate Coptic)
  Validate an nth-weekday request for a Coptic month.

  Totality: total
  Visibility: public export
weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
  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 Coptic
  Construct a Coptic Sunday-based week date under static validity evidence.

  Totality: total
  Visibility: public export
refineWeekDate : WeekNumber -> DayOfWeek -> Year -> Either CopticDateError (CalendarDate Coptic)
  Validate a runtime Coptic Sunday-based week date.

  Totality: total
  Visibility: public export