Idris2Doc : IotaTime.Calendar.Julian

IotaTime.Calendar.Julian

(source)
Definitions
data Julian : Type
  The proleptic Julian calendar, supported from January 1, 45 BC.

  Totality: total
  Visibility: public export
  Constructor: 
JulianCalendar : Julian

  Hint: 
Calendar Julian
data JulianMonth : Type
  Totality: total
  Visibility: public export
  Constructors:
  
January : JulianMonth
  
February : JulianMonth
  
March : JulianMonth
  
April : JulianMonth
  
May : JulianMonth
  
June : JulianMonth
  
July : JulianMonth
  
August : JulianMonth
  
September : JulianMonth
  
October : JulianMonth
  
November : JulianMonth
  
December : JulianMonth

  Hints:
  
Eq JulianMonth
  
Ord JulianMonth
  
Show JulianMonth
monthNumber : JulianMonth -> Integer
  Totality: total
  Visibility: public export
record JulianDate : Type
  Totality: total
  Visibility: export
  Constructor: 
MkJulianDate : (daysSinceEpoch : Integer) -> (0 _ : So (daysSinceEpoch >= -746631)) -> JulianDate

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

  Hints:
  
ApplyPeriod JulianDate
  
CalendarNavigation JulianDate
  
CalendarValue JulianDate
  
Eq JulianDate
  
HasCalendar JulianDate
  
HasCalendarBridge JulianDate
  
Ord JulianDate
  
PeriodTarget JulianDate
  
Show JulianDate
isLeapYear : Year -> Bool
  Whether a Julian year is divisible by four and therefore leap.

  Totality: total
  Visibility: public export
maxDaysInMonth : JulianMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
epochDay : Integer
  The Julian calendar epoch day, representing January 1, 45 BC.

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

  Totality: total
  Visibility: public export
data JulianDateError : Type
  Failures produced while refining untrusted Julian date data.

  Totality: total
  Visibility: public export
  Constructors:
  
InvalidJulianDate : DayOfMonth -> JulianMonth -> Year -> JulianDateError
  
InvalidJulianDayCount : Integer -> JulianDateError
  
InvalidJulianNthDay : DayNth -> DayOfWeek -> JulianMonth -> Year -> JulianDateError
  
InvalidJulianWeekDate : WeekNumber -> DayOfWeek -> Year -> JulianDateError
refineDate : DayOfMonth -> JulianMonth -> Year -> Either JulianDateError (CalendarDate Julian)
  Validate runtime day, month, and year components as a Julian date.

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

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

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

  Totality: total
  Visibility: public export
refineNthDay : DayNth -> DayOfWeek -> JulianMonth -> Year -> Either JulianDateError (CalendarDate Julian)
  Validate an nth-weekday request for a Julian 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 Julian
  Construct a Julian Sunday-based week date under static validity evidence.

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

  Totality: total
  Visibility: public export