IotaTime.Pattern.Instant

Definitions

record InstantPattern : Type -> Type

  A Gregorian date-time pattern adapted to parse and format UTC instants.

Totality: total
Visibility: export
Constructor: 

MkInstantPattern : Pattern state (CalendarDateTime Gregorian) -> InstantPattern state

Projection: 

.calendarPattern : InstantPattern state -> Pattern state (CalendarDateTime Gregorian)

instantPattern : Pattern state (CalendarDateTime Gregorian) -> InstantPattern state

  Build an Instant pattern from a Gregorian CalendarDateTime pattern.

Totality: total
Visibility: public export

parseInstant : InstantPattern state -> String -> Either PatternError Instant

  Parse an Instant, treating the underlying Gregorian date-time as UTC.

Totality: total
Visibility: public export

formatInstant : InstantPattern state -> Instant -> Either CalendarConversionError String

  Format an Instant in UTC. Instants outside the Gregorian calendar's
  supported range return the existing typed calendar conversion error.

Totality: total
Visibility: public export

pInstant : InstantPattern (DateFields, TimeFields)

  ISO-8601 UTC at whole-second precision: yyyy-MM-ddTHH:mm:ssZ.

Totality: total
Visibility: public export

pInstantNano : InstantPattern (DateFields, TimeFields)

  ISO-8601 UTC with nine fractional digits:
  yyyy-MM-ddTHH:mm:ss.fffffffffZ.

Totality: total
Visibility: public export