IotaTime.OffsetDateTime

Reexports

Definitions

record OffsetDateTimeRep : (calendar : Type) -> Calendar calendar -> Type

Totality: total
Visibility: export
Constructor: 

MkOffsetDateTime : CalendarDateTime calendar -> Offset -> OffsetDateTimeRep calendar cal

Projections:

.localValue : OffsetDateTimeRep calendar cal -> CalendarDateTime calendar

.offsetValue : OffsetDateTimeRep calendar cal -> Offset

Hints:

Eq (CalendarDateTime calendar) => Eq (OffsetDateTimeRep calendar cal)

HasCalendarBridge (CalendarDate calendar) => Eq (CalendarDate calendar) => Ord (OffsetDateTimeRep calendar cal)

HasCalendarBridge (CalendarDate calendar) => Show (OffsetDateTimeRep calendar cal)

OffsetDateTime : (calendar : Type) -> Calendar calendar => Type

Totality: total
Visibility: public export

atOffset : {auto cal : Calendar calendar} -> CalendarDateTime calendar -> Offset -> OffsetDateTime calendar

  Associate a calendar-local date and time with its displacement from UTC.

Totality: total
Visibility: export

fromCalendarDateTimeWithOffset : {auto cal : Calendar calendar} -> CalendarDateTime calendar -> Offset -> OffsetDateTime calendar

  HodaTime-compatible constructor from a local calendar date-time and offset.

Totality: total
Visibility: public export

localDateTime : {auto cal : Calendar calendar} -> OffsetDateTime calendar -> CalendarDateTime calendar

Totality: total
Visibility: export

toCalendarDateTime : {auto cal : Calendar calendar} -> OffsetDateTime calendar -> CalendarDateTime calendar

Totality: total
Visibility: public export

offsetOf : {auto cal : Calendar calendar} -> OffsetDateTime calendar -> Offset

Totality: total
Visibility: export

offset : {auto cal : Calendar calendar} -> OffsetDateTime calendar -> Offset

Totality: total
Visibility: public export

offsetDateTimeLocalPart : {auto cal : Calendar calendar} -> (valueDateTime : CalendarDateTime calendar) -> (valueOffset : Offset) -> toCalendarDateTime (fromCalendarDateTimeWithOffset valueDateTime valueOffset) = valueDateTime

  Extracting the local date-time after construction returns the supplied value.

Totality: total
Visibility: public export

offsetDateTimeOffsetPart : {auto cal : Calendar calendar} -> (valueDateTime : CalendarDateTime calendar) -> (valueOffset : Offset) -> offset (fromCalendarDateTimeWithOffset valueDateTime valueOffset) = valueOffset

  Extracting the offset after construction returns the supplied offset.

Totality: total
Visibility: public export

offsetDateTimeRoundTrip : {auto cal : Calendar calendar} -> (value : OffsetDateTime calendar) -> fromCalendarDateTimeWithOffset (toCalendarDateTime value) (offset value) = value

  Reconstructing an offset date-time from its projections is exact.

Totality: total
Visibility: public export

toInstant : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => OffsetDateTime calendar -> Instant

  Resolve an offset date-time to its unique point on the global timeline.

Totality: total
Visibility: public export

fromInstant : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Offset -> Instant -> Either CalendarConversionError (OffsetDateTime calendar)

  Display an instant using a calendar and offset. Conversion can fail only
  when the resulting local day lies outside the calendar's supported range.

Totality: total
Visibility: export

fromInstantWithOffset : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Instant -> Offset -> Either CalendarConversionError (OffsetDateTime calendar)

  HodaTime-compatible constructor with instant-first argument order.

Totality: total
Visibility: public export

withOffset : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Offset -> OffsetDateTime calendar -> Either CalendarConversionError (OffsetDateTime calendar)

  Change the displayed offset while preserving the represented instant.

Totality: total
Visibility: public export

withCalendar : {auto sourceCal : Calendar source} -> {auto targetCal : Calendar target} -> HasCalendarBridge (CalendarDate source) => HasCalendarBridge (CalendarDate target) => OffsetDateTime source -> Either CalendarConversionError (OffsetDateTime target)

  Change the calendar while preserving the local time, offset, and instant.

Totality: total
Visibility: public export