IotaTime.Locale

Definitions

record Locale : Type

  Locale data used by Gregorian date and local-time patterns.
  
  Values are acquired from the operating system or supplied by the built-in
  locales. The representation is hidden so all name tables retain their sizes.

Totality: total
Visibility: export
Constructor: 

MkLocale : String -> Vect 12 String -> Vect 12 String -> Vect 7 String -> Vect 7 String -> String -> String -> String -> String -> String -> Locale

Projections:

.storedAmName : Locale -> String

.storedDayNames : Locale -> Vect 7 String

.storedDayNamesShort : Locale -> Vect 7 String

.storedLocaleId : Locale -> String

.storedMonthNames : Locale -> Vect 12 String

.storedMonthNamesShort : Locale -> Vect 12 String

.storedPmName : Locale -> String

.storedRawDateFormat : Locale -> String

.storedRawDateTimeFormat : Locale -> String

.storedRawTimeFormat : Locale -> String

Hints:

Eq Locale

Show Locale

localeId : Locale -> String

  The operating-system identifier or stable identifier of a locale.

Totality: total
Visibility: public export

monthNames : Locale -> Vect 12 String

  Full Gregorian month names ordered January through December.

Totality: total
Visibility: public export

monthNamesShort : Locale -> Vect 12 String

  Abbreviated Gregorian month names ordered January through December.

Totality: total
Visibility: public export

dayNames : Locale -> Vect 7 String

  Full weekday names ordered Sunday through Saturday.

Totality: total
Visibility: public export

dayNamesShort : Locale -> Vect 7 String

  Abbreviated weekday names ordered Sunday through Saturday.

Totality: total
Visibility: public export

amName : Locale -> String

  The locale's ante-meridiem designator, which may be empty.

Totality: total
Visibility: public export

pmName : Locale -> String

  The locale's post-meridiem designator, which may be empty.

Totality: total
Visibility: public export

rawDateFormat : Locale -> String

Totality: total
Visibility: export

rawTimeFormat : Locale -> String

Totality: total
Visibility: export

rawDateTimeFormat : Locale -> String

Totality: total
Visibility: export

data LocaleError : Type

  A failure to acquire locale data from the operating system.

Totality: total
Visibility: public export
Constructors:

LocaleNotFound : String -> LocaleError

LocalePlatformError : String -> LocaleError

Hints:

Eq LocaleError

Show LocaleError

localeByName : String -> IO (Either LocaleError Locale)

  Read a named locale from the operating system locale database.

Totality: total
Visibility: public export

currentLocale : IO (Either LocaleError Locale)

  Read the locale selected by LC_ALL, LC_TIME, or LANG.

Totality: total
Visibility: public export

enUS : Locale

  Built-in United States English locale data.

Totality: total
Visibility: public export

deDE : Locale

  Built-in German locale data for Germany.

Totality: total
Visibility: public export

jaJP : Locale

  Built-in Japanese locale data for Japan.

Totality: total
Visibility: public export