IotaTime.ZonedDateTime

Reexports

Definitions

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

Totality: total
Visibility: export
Constructor: 

MkZonedDateTime : OffsetDateTime calendar -> TimeZone -> ZonedDateTimeRep calendar cal

Projections:

.zonedValue : ZonedDateTimeRep calendar cal -> OffsetDateTime calendar

.zonedZone : ZonedDateTimeRep calendar cal -> TimeZone

Hints:

Eq (OffsetDateTime calendar) => Eq (ZonedDateTimeRep calendar cal)

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

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

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

Totality: total
Visibility: public export

inZone : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => TimeZone -> Instant -> Either CalendarConversionError (ZonedDateTime calendar)

  Display an instant in a zone using the zone's effective offset. Conversion
  fails only when the resulting local day is outside the calendar's range.

Totality: total
Visibility: export

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

  HodaTime-compatible instant-first constructor.

Totality: total
Visibility: public export

zonedOffsetDateTime : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> OffsetDateTime calendar

Totality: total
Visibility: export

zonedLocalDateTime : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> CalendarDateTime calendar

Totality: total
Visibility: export

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

Totality: total
Visibility: public export

toCalendarDate : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> CalendarDate calendar

Totality: total
Visibility: public export

toLocalTime : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> LocalTime

Totality: total
Visibility: public export

year : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Year

Totality: total
Visibility: public export

month : {auto cal : Calendar calendar} -> (value : ZonedDateTime calendar) -> MonthRep (year value)

Totality: total
Visibility: public export

day : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> DayOfMonth

Totality: total
Visibility: public export

hour : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Hour

Totality: total
Visibility: public export

minute : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Minute

Totality: total
Visibility: public export

second : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Second

Totality: total
Visibility: public export

nanosecond : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Nanosecond

Totality: total
Visibility: public export

zonedOffset : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> Offset

Totality: total
Visibility: export

zonedInstant : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => ZonedDateTime calendar -> Instant

Totality: total
Visibility: export

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

Totality: total
Visibility: public export

zoneOf : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> TimeZone

Totality: total
Visibility: export

zoneId : {auto cal : Calendar calendar} -> ZonedDateTime calendar -> String

Totality: total
Visibility: public export

inDst : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => ZonedDateTime calendar -> Bool

Totality: total
Visibility: public export

zoneAbbreviation : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => ZonedDateTime calendar -> String

Totality: total
Visibility: public export

data ZonedMapping : (calendar : Type) -> Calendar calendar -> Type

  The complete result of resolving a local date-time into a zone.

Totality: total
Visibility: public export
Constructors:

ZonedSkipped : ZonedMapping calendar cal

ZonedUnambiguous : ZonedDateTime calendar -> ZonedMapping calendar cal

ZonedAmbiguous : ZonedDateTime calendar -> ZonedDateTime calendar -> List (ZonedDateTime calendar) -> ZonedMapping calendar cal

resolveLocal : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => TimeZone -> CalendarDateTime calendar -> ZonedMapping calendar cal

  Resolve a local date-time without choosing silently between skipped or
  ambiguous mappings.

Totality: total
Visibility: public export

fromCalendarDateTimeAll : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => CalendarDateTime calendar -> TimeZone -> List (ZonedDateTime calendar)

  Return every valid mapping of a local calendar date-time, in instant order.

Totality: total
Visibility: public export

data ZonedDateTimeError : Type

Totality: total
Visibility: public export
Constructors:

DateTimeDoesNotExist : ZonedDateTimeError

DateTimeAmbiguous : ZonedDateTimeError

LenientResolutionFailed : ZonedDateTimeError

ZonedCalendarOutOfRange : CalendarConversionError -> ZonedDateTimeError

fromCalendarDateTimeStrictly : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => CalendarDateTime calendar -> TimeZone -> Either ZonedDateTimeError (ZonedDateTime calendar)

  Resolve only a unique local mapping. Skipped and ambiguous values are
  returned as typed errors rather than exceptions.

Totality: total
Visibility: public export

fromCalendarDateTimeLeniently : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => CalendarDateTime calendar -> TimeZone -> Either ZonedDateTimeError (ZonedDateTime calendar)

  Apply HodaTime's lenient rules: choose the earliest ambiguous mapping and
  shift skipped values forward by the transition gap.

Totality: total
Visibility: public export

withZone : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => TimeZone -> ZonedDateTime calendar -> Either CalendarConversionError (ZonedDateTime calendar)

  Change zones 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) => ZonedDateTime source -> Either CalendarConversionError (ZonedDateTime target)

  Change calendars while preserving the instant and zone.

Totality: total
Visibility: public export

addZonedDuration : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Duration -> ZonedDateTime calendar -> Either CalendarConversionError (ZonedDateTime calendar)

  Add elapsed time on the global timeline, then re-evaluate the zone offset.

Totality: total
Visibility: export

add : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => ZonedDateTime calendar -> Duration -> Either CalendarConversionError (ZonedDateTime calendar)

  Add fixed elapsed time, following HodaTime's value-first argument order.

Totality: total
Visibility: public export

subtractZonedDuration : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Duration -> ZonedDateTime calendar -> Either CalendarConversionError (ZonedDateTime calendar)

  Subtract elapsed time on the global timeline, then re-evaluate the zone offset.

Totality: total
Visibility: export

minus : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => ZonedDateTime calendar -> Duration -> Either CalendarConversionError (ZonedDateTime calendar)

  Subtract fixed elapsed time, following HodaTime's value-first argument order.

Totality: total
Visibility: public export