Idris2Doc : IotaTime.Calendar.Hebrew

IotaTime.Calendar.Hebrew

(source)
Definitions
data HebrewNumbering : Type
  Hebrew month numbering: civil begins at Tishri, scriptural at Nisan.

  Totality: total
  Visibility: public export
  Constructors:
  
Civil : HebrewNumbering
  
Scriptural : HebrewNumbering

  Hints:
  
ApplyPeriod (HebrewDate numbering)
  
KnownHebrewNumbering numbering => Calendar (Hebrew numbering)
  
KnownHebrewNumbering numbering => CalendarNavigation (HebrewDate numbering)
  
KnownHebrewNumbering numbering => CalendarValue (HebrewDate numbering)
  
Eq (HebrewMonth numbering valueYear)
  
Eq (HebrewDate numbering)
  
HasCalendar (HebrewDate numbering)
  
HasCalendarBridge (HebrewDate numbering)
  
Ord (HebrewMonth numbering valueYear)
  
Ord (HebrewDate numbering)
  
PeriodTarget (HebrewDate numbering)
  
Show (HebrewMonth numbering valueYear)
  
Show (HebrewDate numbering)
interface KnownHebrewNumbering : HebrewNumbering -> Type
  Evidence exposing the starting month for a Hebrew numbering system.

  Parameters: numbering
Methods:
  
numberingStart : Integer

Implementations:
  
KnownHebrewNumbering Civil
  
KnownHebrewNumbering Scriptural
numberingStart : KnownHebrewNumbering numbering => Integer
  Totality: total
  Visibility: public export
data Hebrew : HebrewNumbering -> Type
  The Hebrew calendar indexed by its month-numbering convention.

  Totality: total
  Visibility: public export
  Constructor: 
HebrewCalendar : Hebrew numbering

  Hint: 
KnownHebrewNumbering numbering => Calendar (Hebrew numbering)
HebrewCivil : Type
  Totality: total
  Visibility: public export
HebrewScriptural : Type
  Totality: total
  Visibility: public export
isLeapYear : Year -> Bool
  Totality: total
  Visibility: public export
data HebrewMonth : HebrewNumbering -> Year -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Tishri : HebrewMonth numbering valueYear
  
Cheshvan : HebrewMonth numbering valueYear
  
Kislev : HebrewMonth numbering valueYear
  
Tevet : HebrewMonth numbering valueYear
  
Shevat : HebrewMonth numbering valueYear
  
AdarI : {auto 0 _ : So (isLeapYear valueYear)} -> HebrewMonth numbering valueYear
  
Adar : HebrewMonth numbering valueYear
  
Nisan : HebrewMonth numbering valueYear
  
Iyar : HebrewMonth numbering valueYear
  
Sivan : HebrewMonth numbering valueYear
  
Tammuz : HebrewMonth numbering valueYear
  
Av : HebrewMonth numbering valueYear
  
Elul : HebrewMonth numbering valueYear

  Hints:
  
Eq (HebrewMonth numbering valueYear)
  
Ord (HebrewMonth numbering valueYear)
  
Show (HebrewMonth numbering valueYear)
calendarIndex : HebrewMonth numbering valueYear -> Integer
  Totality: total
  Visibility: public export
showMonth : HebrewMonth numbering valueYear -> String
  Totality: total
  Visibility: export
data HebrewMonthName : Type
  A non-dependent Hebrew month name used at runtime refinement boundaries.

  Totality: total
  Visibility: public export
  Constructors:
  
TishriName : HebrewMonthName
  
CheshvanName : HebrewMonthName
  
KislevName : HebrewMonthName
  
TevetName : HebrewMonthName
  
ShevatName : HebrewMonthName
  
AdarIName : HebrewMonthName
  
AdarName : HebrewMonthName
  
NisanName : HebrewMonthName
  
IyarName : HebrewMonthName
  
SivanName : HebrewMonthName
  
TammuzName : HebrewMonthName
  
AvName : HebrewMonthName
  
ElulName : HebrewMonthName

  Hint: 
Eq HebrewMonthName
monthName : HebrewMonth numbering valueYear -> HebrewMonthName
  Totality: total
  Visibility: public export
monthNumber : KnownHebrewNumbering numbering => HebrewMonth numbering year -> Integer
  Totality: total
  Visibility: public export
monthsElapsed : Year -> Integer
  Totality: total
  Visibility: public export
elapsedDays : Year -> Integer
  Totality: total
  Visibility: public export
firstDayOfYear : Year -> Integer
  Totality: total
  Visibility: public export
daysInYear : Year -> Integer
  Totality: total
  Visibility: public export
isCheshvanLong : Year -> Bool
  Totality: total
  Visibility: public export
isKislevShort : Year -> Bool
  Totality: total
  Visibility: public export
monthLengthByIndex : Year -> Integer -> Integer
  Totality: total
  Visibility: public export
maxDaysInMonth : HebrewMonth numbering year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidDay : DayOfMonth -> (valueYear : Year) -> HebrewMonth numbering valueYear -> Bool
  Totality: total
  Visibility: public export
epochDay : Integer
  The Hebrew calendar epoch day, representing 1 Tishri 1.

  Totality: total
  Visibility: public export
record HebrewDate : HebrewNumbering -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkHebrewDate : (daysSinceEpoch : Integer) -> (0 _ : So (daysSinceEpoch >= -2103607)) -> HebrewDate numbering

  Projections:
  
.daysSinceEpoch : HebrewDate numbering -> Integer
  
0 .validDays : ({rec:0} : HebrewDate numbering) -> So (daysSinceEpoch {rec:0} >= -2103607)

  Hints:
  
ApplyPeriod (HebrewDate numbering)
  
KnownHebrewNumbering numbering => CalendarNavigation (HebrewDate numbering)
  
KnownHebrewNumbering numbering => CalendarValue (HebrewDate numbering)
  
Eq (HebrewDate numbering)
  
HasCalendar (HebrewDate numbering)
  
HasCalendarBridge (HebrewDate numbering)
  
Ord (HebrewDate numbering)
  
PeriodTarget (HebrewDate numbering)
  
Show (HebrewDate numbering)
isValidDate : DayOfMonth -> (valueYear : Year) -> HebrewMonth numbering valueYear -> Bool
  Totality: total
  Visibility: public export
calendarDate' : {auto known : KnownHebrewNumbering numbering} -> (valueDay : DayOfMonth) -> (valueYear : Year) -> (valueMonth : HebrewMonth numbering valueYear) -> {auto 0 _ : So (isValidDate valueDay valueYear valueMonth)} -> CalendarDate (Hebrew numbering)
  Construct a statically validated Hebrew date in the selected numbering.
  The month is indexed by the year, making Adar I unavailable in common years.

  Totality: total
  Visibility: public export
calendarDate : (valueDay : DayOfMonth) -> (valueYear : Year) -> (valueMonth : HebrewMonth Civil valueYear) -> {auto 0 _ : So (isValidDate valueDay valueYear valueMonth)} -> CalendarDate HebrewCivil
  Construct a statically validated civil-numbered Hebrew date.

  Totality: total
  Visibility: public export
data HebrewDateError : Type
  Failures produced while refining untrusted Hebrew date data.

  Totality: total
  Visibility: public export
  Constructors:
  
InvalidHebrewMonth : HebrewMonthName -> Year -> HebrewDateError
  
InvalidHebrewDate : DayOfMonth -> HebrewMonthName -> Year -> HebrewDateError
  
InvalidHebrewDayCount : Integer -> HebrewDateError
  
InvalidHebrewNthDay : DayNth -> HebrewMonthName -> Year -> HebrewDateError
  
InvalidHebrewWeekDate : WeekNumber -> Year -> HebrewDateError
refineMonth : (valueYear : Year) -> HebrewMonthName -> Either HebrewDateError (HebrewMonth numbering valueYear)
  Refine a runtime month name into a year-indexed Hebrew month.
  Adar I is rejected when the supplied year is not leap.

  Totality: total
  Visibility: public export
refineDate' : {auto known : KnownHebrewNumbering numbering} -> DayOfMonth -> HebrewMonthName -> Year -> Either HebrewDateError (CalendarDate (Hebrew numbering))
  Validate runtime date components in the selected Hebrew numbering.

  Totality: total
  Visibility: public export
refineDate : DayOfMonth -> HebrewMonthName -> Year -> Either HebrewDateError (CalendarDate HebrewCivil)
  Validate runtime date components using civil Hebrew numbering.

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

  Totality: total
  Visibility: public export
fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate HebrewCivil
  Totality: total
  Visibility: public export
refineDays' : {auto known : KnownHebrewNumbering numbering} -> Integer -> Either HebrewDateError (CalendarDate (Hebrew numbering))
  Validate a runtime Hebrew day count in the selected numbering.

  Totality: total
  Visibility: public export
refineDays : Integer -> Either HebrewDateError (CalendarDate HebrewCivil)
  Totality: total
  Visibility: public export
nthDayOfMonth : DayNth -> DayOfWeek -> (valueYear : Year) -> HebrewMonth numbering valueYear -> DayOfMonth
  Totality: total
  Visibility: public export
isValidNthDay : DayNth -> DayOfWeek -> (valueYear : Year) -> HebrewMonth numbering valueYear -> Bool
  Totality: total
  Visibility: public export
fromNthDay' : {auto {conArg:7553} : KnownHebrewNumbering numbering} -> (nth : DayNth) -> (target : DayOfWeek) -> (valueYear : Year) -> (valueMonth : HebrewMonth numbering valueYear) -> {auto 0 _ : So (isValidNthDay nth target valueYear valueMonth)} -> CalendarDate (Hebrew numbering)
  Construct the nth requested weekday in a Hebrew month using the selected
  numbering convention.

  Totality: total
  Visibility: public export
fromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueYear : Year) -> (valueMonth : HebrewMonth Civil valueYear) -> {auto 0 _ : So (isValidNthDay nth target valueYear valueMonth)} -> CalendarDate HebrewCivil
  Totality: total
  Visibility: public export
refineNthDay' : {auto known : KnownHebrewNumbering numbering} -> DayNth -> DayOfWeek -> Year -> HebrewMonthName -> Either HebrewDateError (CalendarDate (Hebrew numbering))
  Validate an nth-weekday request in the selected Hebrew numbering.

  Totality: total
  Visibility: public export
refineNthDay : DayNth -> DayOfWeek -> Year -> HebrewMonthName -> Either HebrewDateError (CalendarDate HebrewCivil)
  Totality: total
  Visibility: public export
weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
  Totality: total
  Visibility: public export
isValidWeekDate : KnownHebrewNumbering numbering => WeekNumber -> DayOfWeek -> Year -> Bool
  Totality: total
  Visibility: public export
fromWeekDate' : {auto {conArg:7847} : KnownHebrewNumbering numbering} -> (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate (Hebrew numbering)
  Construct a Sunday-based Hebrew week date in the selected numbering.

  Totality: total
  Visibility: public export
fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate HebrewCivil
  Totality: total
  Visibility: public export
refineWeekDate' : {auto known : KnownHebrewNumbering numbering} -> WeekNumber -> DayOfWeek -> Year -> Either HebrewDateError (CalendarDate (Hebrew numbering))
  Validate a runtime Hebrew week date in the selected numbering.

  Totality: total
  Visibility: public export
refineWeekDate : WeekNumber -> DayOfWeek -> Year -> Either HebrewDateError (CalendarDate HebrewCivil)
  Totality: total
  Visibility: public export