IotaTime.Pattern.Calendar

Definitions

data PatternMonthNameSource : Nat -> Type

  Selects whether locale-backed patterns use the locale's twelve Gregorian
  month names or the selected calendar's canonical names.

Totality: total
Visibility: public export
Constructors:

GregorianLocaleMonthNames : (0 _ : monthCount = 12) -> PatternMonthNameSource monthCount

CanonicalCalendarMonthNames : PatternMonthNameSource monthCount

interface CalendarPattern : Type -> Type

  Calendar-specific projection and runtime refinement used by date patterns.

Parameters: calendar
Constraints: Calendar calendar
Methods:

patternMonthCount : Nat

patternMonthNames : Vect patternMonthCount String

patternMonthAbbreviations : Vect patternMonthCount String

patternMonthNameSource : PatternMonthNameSource patternMonthCount

patternMonthIndex : CalendarDate calendar -> Fin patternMonthCount

patternWeekdayIndex : CalendarDate calendar -> Fin 7

refinePatternDate : Integer -> Integer -> Integer -> Either PatternError (CalendarDate calendar)

Implementations:

CalendarPattern Gregorian

CalendarPattern Julian

CalendarPattern Coptic

KnownIslamicLeapPattern pattern => CalendarPattern (Islamic pattern)

KnownIslamicLeapPattern pattern => CalendarPattern (CivilIslamic pattern)

CalendarPattern Persian

CalendarPattern (ArithmeticPersian rule)

KnownHebrewNumbering numbering => CalendarPattern (Hebrew numbering)

patternMonthCount : CalendarPattern calendar => Nat

Totality: total
Visibility: public export

patternMonthNames : {auto __con : CalendarPattern calendar} -> Vect patternMonthCount String

Totality: total
Visibility: public export

patternMonthAbbreviations : {auto __con : CalendarPattern calendar} -> Vect patternMonthCount String

Totality: total
Visibility: public export

patternMonthNameSource : {auto __con : CalendarPattern calendar} -> PatternMonthNameSource patternMonthCount

Totality: total
Visibility: public export

patternMonthIndex : {auto __con : CalendarPattern calendar} -> CalendarDate calendar -> Fin patternMonthCount

Totality: total
Visibility: public export

patternWeekdayIndex : {auto __con : CalendarPattern calendar} -> CalendarDate calendar -> Fin 7

Totality: total
Visibility: public export

refinePatternDate : {auto __con : CalendarPattern calendar} -> Integer -> Integer -> Integer -> Either PatternError (CalendarDate calendar)

Totality: total
Visibility: public export