
  0 | module IotaTime.Pattern.OffsetDateTime
  1 | 
  2 | import IotaTime.OffsetDateTime
  3 | import IotaTime.Pattern
  4 | import IotaTime.Pattern.Calendar
  5 | import IotaTime.Pattern.CalendarDate
  6 | import IotaTime.Pattern.CalendarDateTime
  7 | import IotaTime.Pattern.LocalTime
  8 | import IotaTime.Pattern.Offset
  9 | 
 10 | %default total
 11 | 
 12 | ||| Combine independently typed local date-time and UTC-offset patterns.
 13 | public export
 14 | offsetDateTimePattern :
 15 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 16 |   Pattern localState (CalendarDateTime calendar) ->
 17 |   Pattern offsetState Offset ->
 18 |   Pattern (localState, offsetState) (OffsetDateTime calendar)
 19 | offsetDateTimePattern = pairPattern localDateTime offsetOf atOffset
 20 | 
 21 | ||| ISO local date-time followed by an ISO offset, for example
 22 | ||| `2024-04-23T09:00:00+02:00`.
 23 | public export
 24 | pOffsetDateTime : {calendar : Type} ->
 25 |   {auto patterned : CalendarPattern calendar} ->
 26 |   Pattern ((DateFields, TimeFields), Offset) (OffsetDateTime calendar)
 27 | pOffsetDateTime = offsetDateTimePattern ps pOffset