IotaTime.Pattern.CalendarDate

Definitions

record DateFieldsRep : Type

  Intermediate fields accumulated while parsing a calendar date.

Totality: total
Visibility: export
Constructor: 

MkDateFields : Integer -> Integer -> Integer -> {default Nothing _ : Maybe (Fin 7)} -> DateFieldsRep

Projections:

.parsedDay : DateFieldsRep -> Integer

.parsedMonth : DateFieldsRep -> Integer

.parsedWeekday : DateFieldsRep -> Maybe (Fin 7)

.parsedYear : DateFieldsRep -> Integer

DateFields : Type

  Opaque intermediate state used by calendar-date patterns.

Totality: total
Visibility: public export

dateFields : Integer -> Integer -> Integer -> DateFields

  Seed omitted year, month, and day fields for `parseWith`.
  Parsed fields replace the corresponding seed values; final calendar-date
  validation still occurs after parsing.

Totality: total
Visibility: public export

pyear : {auto patterned : CalendarPattern calendar} -> Nat -> Pattern DateFields (CalendarDate calendar)

  A numeric year field with the requested output width and up to four input digits.

Totality: total
Visibility: public export

pyyyy : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A four-digit numeric year field.

Totality: total
Visibility: public export

pyy : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A two-digit year field resolved to the century nearest the initial year.

Totality: total
Visibility: public export

pmonthNum : {auto patterned : CalendarPattern calendar} -> Nat -> Pattern DateFields (CalendarDate calendar)

  A numeric month field bounded by the selected calendar's month count.

Totality: total
Visibility: public export

pMM : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A two-digit numeric month field.

Totality: total
Visibility: public export

pMonthName : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Vect size String -> {auto 0 _ : size = patternMonthCount} -> Pattern DateFields (CalendarDate calendar)

  A calendar month field using supplied names in calendar order.
  
  Parsing tries non-empty names longest-first. Equal or duplicate names retain
  table order and select the first matching month. Formatting uses the supplied
  name verbatim, including an empty name.

Totality: total
Visibility: public export

pMMMM : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A calendar-specific full month-name field.

Totality: total
Visibility: public export

pMMM : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A calendar-specific abbreviated month-name field.

Totality: total
Visibility: public export

pday : {auto patterned : CalendarPattern calendar} -> Nat -> Pattern DateFields (CalendarDate calendar)

  A numeric day-of-month field with the requested width.

Totality: total
Visibility: public export

pdd : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A two-digit day-of-month field.

Totality: total
Visibility: public export

pdaySpace : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A two-character day-of-month field padded with a leading space.

Totality: total
Visibility: public export

pDayName : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Vect 7 String -> Pattern DateFields (CalendarDate calendar)

  A calendar weekday field using supplied Sunday-first names.
  
  Parsing consumes and validates a name structurally; the date fields determine
  the resulting date. Non-empty names are tried longest-first; formatting uses
  the supplied name verbatim.

Totality: total
Visibility: public export

pVerifiedDayName : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Vect 7 String -> Pattern DateFields (CalendarDate calendar)

  A calendar weekday field that rejects a parsed name inconsistent with the
  resulting date. Names are supplied in Sunday-first order.

Totality: total
Visibility: public export

pdddd : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A full English weekday-name field for the selected calendar.

Totality: total
Visibility: public export

pddd : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  An abbreviated English weekday-name field for the selected calendar.

Totality: total
Visibility: public export

pddddVerified : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  A full English weekday-name field verified against the resulting date.

Totality: total
Visibility: public export

pdddVerified : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  An abbreviated English weekday-name field verified against the resulting date.

Totality: total
Visibility: public export

pMMMM' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  A full month-name field using locale names when the selected calendar
  shares Gregorian month identities, and canonical names otherwise.

Totality: total
Visibility: public export

pMMM' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  An abbreviated month-name field using locale names when the selected
  calendar shares Gregorian month identities, and canonical names otherwise.

Totality: total
Visibility: public export

pdddd' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  A full locale weekday-name field for the selected calendar.

Totality: total
Visibility: public export

pddd' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  An abbreviated locale weekday-name field for the selected calendar.

Totality: total
Visibility: public export

pddddVerified' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  A full locale weekday-name field verified against the resulting date.

Totality: total
Visibility: public export

pdddVerified' : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Pattern DateFields (CalendarDate calendar)

  An abbreviated locale weekday-name field verified against the resulting date.

Totality: total
Visibility: public export

pd : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  The numeric `dd/MM/yyyy` date pattern.

Totality: total
Visibility: public export

pD : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  The long `weekday, dd month yyyy` date pattern.

Totality: total
Visibility: public export

pR : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  The ISO-style `yyyy-MM-dd` date pattern.

Totality: total
Visibility: public export

pmonthDay : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  The `month dd` pattern without a year field.

Totality: total
Visibility: public export

pyearMonth : {auto patterned : CalendarPattern calendar} -> Pattern DateFields (CalendarDate calendar)

  The `yyyy month` pattern without a day field.

Totality: total
Visibility: public export