IotaTime.Pattern.CalendarDateTime

Definitions

calendarDateTimePattern : {auto patterned : CalendarPattern calendar} -> Pattern dateState (CalendarDate calendar) -> Pattern timeState LocalTime -> Pattern (dateState, timeState) (CalendarDateTime calendar)

  Combine independently typed calendar-date and local-time patterns.

Totality: total
Visibility: public export

ps : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Sortable ISO local date-time: `yyyy-MM-ddTHH:mm:ss`.

Totality: total
Visibility: public export

po : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Sortable ISO local date-time with nine fractional digits.

Totality: total
Visibility: public export

pf : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Full date with a short 12-hour local time.

Totality: total
Visibility: public export

pF : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Full date with a long 24-hour local time.

Totality: total
Visibility: public export

pg : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Short date with a short 12-hour local time.

Totality: total
Visibility: public export

pG : {auto patterned : CalendarPattern calendar} -> Pattern (DateFields, TimeFields) (CalendarDateTime calendar)

  Short date with a long 24-hour local time.

Totality: total
Visibility: public export