Idris2Doc : IotaTime.Calendar.Islamic

IotaTime.Calendar.Islamic

(source)
Definitions
data IslamicLeapPattern : Type
  The supported tabular Islamic 30-year leap-cycle assignments.

  Totality: total
  Visibility: public export
  Constructors:
  
Base15 : IslamicLeapPattern
  
Base16 : IslamicLeapPattern
  
Indian : IslamicLeapPattern
  
HabashAlHasib : IslamicLeapPattern

  Hints:
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => ApplyPeriod (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Calendar (IslamicByEpoch epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarNavigation (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarValue (IslamicDate epoch pattern)
  
Eq (IslamicDate epoch pattern)
  
HasCalendar (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => HasCalendarBridge (IslamicDate epoch pattern)
  
Ord (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => PeriodTarget (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Show (IslamicDate epoch pattern)
interface KnownIslamicLeapPattern : IslamicLeapPattern -> Type
  Evidence and leap-year positions for one Islamic leap pattern.

  Parameters: pattern
Methods:
  
leapCycleYears : List Integer

Implementations:
  
KnownIslamicLeapPattern Base15
  
KnownIslamicLeapPattern Base16
  
KnownIslamicLeapPattern Indian
  
KnownIslamicLeapPattern HabashAlHasib
leapCycleYears : KnownIslamicLeapPattern pattern => List Integer
  Totality: total
  Visibility: public export
data IslamicEpoch : Type
  The two conventional epochs used by tabular Islamic calendars.

  Totality: total
  Visibility: public export
  Constructors:
  
Astronomical : IslamicEpoch
  
Civil : IslamicEpoch

  Hints:
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => ApplyPeriod (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Calendar (IslamicByEpoch epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarNavigation (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarValue (IslamicDate epoch pattern)
  
Eq (IslamicDate epoch pattern)
  
HasCalendar (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => HasCalendarBridge (IslamicDate epoch pattern)
  
Ord (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => PeriodTarget (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Show (IslamicDate epoch pattern)
interface KnownIslamicEpoch : IslamicEpoch -> Type
  Evidence for the first timeline day represented by an Islamic epoch.

  Parameters: epoch
Methods:
  
epochDay : Integer
  
dateConstructorName : String

Implementations:
  
KnownIslamicEpoch Astronomical
  
KnownIslamicEpoch Civil
epochDay : KnownIslamicEpoch epoch => Integer
  Totality: total
  Visibility: public export
dateConstructorName : KnownIslamicEpoch epoch => String
  Totality: total
  Visibility: public export
data IslamicByEpoch : IslamicEpoch -> IslamicLeapPattern -> Type
  A tabular Islamic calendar indexed by its epoch and leap-cycle pattern.

  Totality: total
  Visibility: public export
  Constructor: 
IslamicCalendar : IslamicByEpoch epoch pattern

  Hint: 
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Calendar (IslamicByEpoch epoch pattern)
Islamic : IslamicLeapPattern -> Type
  The astronomical-epoch calendar retained by the original iotaTime API.

  Totality: total
  Visibility: public export
CivilIslamic : IslamicLeapPattern -> Type
  A civil-epoch tabular Islamic calendar.

  Totality: total
  Visibility: public export
IslamicBase15 : Type
  Totality: total
  Visibility: public export
IslamicBase16 : Type
  Totality: total
  Visibility: public export
IslamicIndian : Type
  Totality: total
  Visibility: public export
IslamicHabashAlHasib : Type
  Totality: total
  Visibility: public export
IslamicBcl : Type
  Totality: total
  Visibility: public export
CivilIslamicBase15 : Type
  Totality: total
  Visibility: public export
CivilIslamicBase16 : Type
  Totality: total
  Visibility: public export
CivilIslamicIndian : Type
  Totality: total
  Visibility: public export
CivilIslamicHabashAlHasib : Type
  Totality: total
  Visibility: public export
CivilIslamicBcl : Type
  Totality: total
  Visibility: public export
data IslamicMonth : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Muharram : IslamicMonth
  
Safar : IslamicMonth
  
RabiAlAwwal : IslamicMonth
  
RabiAlThani : IslamicMonth
  
JumadaAlAwwal : IslamicMonth
  
JumadaAlThani : IslamicMonth
  
Rajab : IslamicMonth
  
Shaban : IslamicMonth
  
Ramadan : IslamicMonth
  
Shawwal : IslamicMonth
  
DhulQadah : IslamicMonth
  
DhulHijjah : IslamicMonth

  Hints:
  
Eq IslamicMonth
  
Ord IslamicMonth
  
Show IslamicMonth
monthNumber : IslamicMonth -> Integer
  Totality: total
  Visibility: public export
record IslamicDate : IslamicEpoch -> IslamicLeapPattern -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkIslamicDate : (daysSinceEpoch : Integer) -> (0 _ : So (daysSinceEpoch >= islamicEpochDay epoch)) -> IslamicDate epoch pattern

  Projections:
  
.daysSinceEpoch : IslamicDate epoch pattern -> Integer
  
0 .validDays : ({rec:0} : IslamicDate epoch pattern) -> So (daysSinceEpoch {rec:0} >= islamicEpochDay epoch)

  Hints:
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => ApplyPeriod (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarNavigation (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => CalendarValue (IslamicDate epoch pattern)
  
Eq (IslamicDate epoch pattern)
  
HasCalendar (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => HasCalendarBridge (IslamicDate epoch pattern)
  
Ord (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => PeriodTarget (IslamicDate epoch pattern)
  
KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern => Show (IslamicDate epoch pattern)
isLeapYear : KnownIslamicLeapPattern pattern => Year -> Bool
  Totality: total
  Visibility: public export
maxDaysInMonth : KnownIslamicLeapPattern pattern => IslamicMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidDate : KnownIslamicLeapPattern pattern => DayOfMonth -> IslamicMonth -> Year -> Bool
  Totality: total
  Visibility: public export
calendarDate' : {auto known : KnownIslamicLeapPattern pattern} -> (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate (Islamic pattern)
  Construct a statically validated Islamic date for the selected leap pattern.

  Totality: total
  Visibility: public export
calendarDate : (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate IslamicBcl
  Construct a statically validated Base16/BCL Islamic date.

  Totality: total
  Visibility: public export
data IslamicDateError : Type
  Failures produced while refining untrusted Islamic date data.

  Totality: total
  Visibility: public export
  Constructors:
  
InvalidIslamicDate : DayOfMonth -> IslamicMonth -> Year -> IslamicDateError
  
InvalidIslamicDayCount : Integer -> IslamicDateError
  
InvalidIslamicNthDay : DayNth -> DayOfWeek -> IslamicMonth -> Year -> IslamicDateError
  
InvalidIslamicWeekDate : WeekNumber -> DayOfWeek -> Year -> IslamicDateError
refineDate' : {auto known : KnownIslamicLeapPattern pattern} -> DayOfMonth -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate (Islamic pattern))
  Validate runtime date components for the selected Islamic leap pattern.

  Totality: total
  Visibility: public export
refineDate : DayOfMonth -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate IslamicBcl)
  Validate runtime date components using the Base16/BCL leap pattern.

  Totality: total
  Visibility: public export
fromDays' : {auto known : KnownIslamicLeapPattern pattern} -> (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate (Islamic pattern)
  Construct a date in the selected Islamic pattern from a statically valid
  calendar-relative day count.

  Totality: total
  Visibility: public export
fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate IslamicBcl
  Totality: total
  Visibility: public export
refineDays' : {auto known : KnownIslamicLeapPattern pattern} -> Integer -> Either IslamicDateError (CalendarDate (Islamic pattern))
  Validate a runtime day count for the selected Islamic leap pattern.

  Totality: total
  Visibility: public export
refineDays : Integer -> Either IslamicDateError (CalendarDate IslamicBcl)
  Totality: total
  Visibility: public export
civilCalendarDate' : {auto known : KnownIslamicLeapPattern pattern} -> (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate (CivilIslamic pattern)
  Construct a statically validated civil-epoch Islamic date for the selected
  leap pattern.

  Totality: total
  Visibility: public export
civilCalendarDate : (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate CivilIslamicBcl
  Construct a statically validated Base16 civil-epoch Islamic date.

  Totality: total
  Visibility: public export
refineCivilDate' : {auto known : KnownIslamicLeapPattern pattern} -> DayOfMonth -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate (CivilIslamic pattern))
  Validate runtime date components for a selected civil-epoch leap pattern.

  Totality: total
  Visibility: public export
refineCivilDate : DayOfMonth -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate CivilIslamicBcl)
  Validate runtime civil-epoch date components using the Base16 pattern.

  Totality: total
  Visibility: public export
civilFromDays' : {auto known : KnownIslamicLeapPattern pattern} -> (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate (CivilIslamic pattern)
  Construct a civil-epoch date from a statically valid timeline day count.

  Totality: total
  Visibility: public export
civilFromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate CivilIslamicBcl
  Totality: total
  Visibility: public export
refineCivilDays' : {auto known : KnownIslamicLeapPattern pattern} -> Integer -> Either IslamicDateError (CalendarDate (CivilIslamic pattern))
  Validate a runtime timeline day count for a selected civil leap pattern.

  Totality: total
  Visibility: public export
refineCivilDays : Integer -> Either IslamicDateError (CalendarDate CivilIslamicBcl)
  Totality: total
  Visibility: public export
nthDayOfMonth : KnownIslamicLeapPattern pattern => DayNth -> DayOfWeek -> IslamicMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
civilNthDayOfMonth : KnownIslamicLeapPattern pattern => DayNth -> DayOfWeek -> IslamicMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidNthDay : KnownIslamicLeapPattern pattern => DayNth -> DayOfWeek -> IslamicMonth -> Year -> Bool
  Totality: total
  Visibility: public export
isValidCivilNthDay : KnownIslamicLeapPattern pattern => DayNth -> DayOfWeek -> IslamicMonth -> Year -> Bool
  Totality: total
  Visibility: public export
fromNthDay' : {auto known : KnownIslamicLeapPattern pattern} -> (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> CalendarDate (Islamic pattern)
  Construct the nth requested weekday in an Islamic month for the selected
  leap pattern.

  Totality: total
  Visibility: public export
fromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> CalendarDate IslamicBcl
  Totality: total
  Visibility: public export
refineNthDay' : {auto known : KnownIslamicLeapPattern pattern} -> DayNth -> DayOfWeek -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate (Islamic pattern))
  Validate an nth-weekday request for the selected Islamic leap pattern.

  Totality: total
  Visibility: public export
refineNthDay : DayNth -> DayOfWeek -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate IslamicBcl)
  Totality: total
  Visibility: public export
civilFromNthDay' : {auto known : KnownIslamicLeapPattern pattern} -> (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidCivilNthDay nth target valueMonth valueYear)} -> CalendarDate (CivilIslamic pattern)
  Construct the nth requested weekday in a civil-epoch Islamic month.

  Totality: total
  Visibility: public export
civilFromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : IslamicMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidCivilNthDay nth target valueMonth valueYear)} -> CalendarDate CivilIslamicBcl
  Totality: total
  Visibility: public export
refineCivilNthDay' : {auto known : KnownIslamicLeapPattern pattern} -> DayNth -> DayOfWeek -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate (CivilIslamic pattern))
  Totality: total
  Visibility: public export
refineCivilNthDay : DayNth -> DayOfWeek -> IslamicMonth -> Year -> Either IslamicDateError (CalendarDate CivilIslamicBcl)
  Totality: total
  Visibility: public export
weekDateDays : KnownIslamicLeapPattern pattern => WeekNumber -> DayOfWeek -> Year -> Integer
  Totality: total
  Visibility: public export
civilWeekDateDays : KnownIslamicLeapPattern pattern => WeekNumber -> DayOfWeek -> Year -> Integer
  Totality: total
  Visibility: public export
isValidWeekDate : KnownIslamicLeapPattern pattern => WeekNumber -> DayOfWeek -> Year -> Bool
  Totality: total
  Visibility: public export
isValidCivilWeekDate : KnownIslamicLeapPattern pattern => WeekNumber -> DayOfWeek -> Year -> Bool
  Totality: total
  Visibility: public export
fromWeekDate' : {auto known : KnownIslamicLeapPattern pattern} -> (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate (Islamic pattern)
  Construct a Saturday-based Islamic week date for the selected leap pattern.

  Totality: total
  Visibility: public export
fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate IslamicBcl
  Totality: total
  Visibility: public export
refineWeekDate' : {auto known : KnownIslamicLeapPattern pattern} -> WeekNumber -> DayOfWeek -> Year -> Either IslamicDateError (CalendarDate (Islamic pattern))
  Validate a runtime Islamic week date for the selected leap pattern.

  Totality: total
  Visibility: public export
refineWeekDate : WeekNumber -> DayOfWeek -> Year -> Either IslamicDateError (CalendarDate IslamicBcl)
  Totality: total
  Visibility: public export
civilFromWeekDate' : {auto known : KnownIslamicLeapPattern pattern} -> (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidCivilWeekDate week target valueYear)} -> CalendarDate (CivilIslamic pattern)
  Construct a Saturday-based civil-epoch Islamic week date.

  Totality: total
  Visibility: public export
civilFromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidCivilWeekDate week target valueYear)} -> CalendarDate CivilIslamicBcl
  Totality: total
  Visibility: public export
refineCivilWeekDate' : {auto known : KnownIslamicLeapPattern pattern} -> WeekNumber -> DayOfWeek -> Year -> Either IslamicDateError (CalendarDate (CivilIslamic pattern))
  Totality: total
  Visibility: public export
refineCivilWeekDate : WeekNumber -> DayOfWeek -> Year -> Either IslamicDateError (CalendarDate CivilIslamicBcl)
  Totality: total
  Visibility: public export