IotaTime.CalendarDateTime

Definitions

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

  A calendar date paired with a local time of day.

Totality: total
Visibility: public export
Constructor: 

MkCalendarDateTime : CalendarDate calendar -> LocalTime -> CalendarDateTimeRep calendar cal

Projections:

.date : CalendarDateTimeRep calendar cal -> CalendarDate calendar

.time : CalendarDateTimeRep calendar cal -> LocalTime

Hints:

Eq (CalendarDate calendar) => Eq (CalendarDateTimeRep calendar cal)

Ord (CalendarDate calendar) => Ord (CalendarDateTimeRep calendar cal)

Show (CalendarDate calendar) => Show (CalendarDateTimeRep calendar cal)

.date : CalendarDateTimeRep calendar cal -> CalendarDate calendar

Totality: total
Visibility: public export

date : CalendarDateTimeRep calendar cal -> CalendarDate calendar

Totality: total
Visibility: public export

.time : CalendarDateTimeRep calendar cal -> LocalTime

Totality: total
Visibility: public export

time : CalendarDateTimeRep calendar cal -> LocalTime

Totality: total
Visibility: public export

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

  The date-time representation selected by a calendar implementation.

Totality: total
Visibility: public export

on : {auto cal : Calendar calendar} -> LocalTime -> CalendarDate calendar -> CalendarDateTime calendar

  Associate a local time with a date, using time-first argument order.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 0

at : {auto cal : Calendar calendar} -> CalendarDate calendar -> LocalTime -> CalendarDateTime calendar

  Associate a date with a local time, using date-first argument order.

Totality: total
Visibility: public export

atStartOfDay : {auto cal : Calendar calendar} -> CalendarDate calendar -> CalendarDateTime calendar

  Associate a date with midnight at the start of that day.

Totality: total
Visibility: public export

datePart : {auto cal : Calendar calendar} -> CalendarDateTime calendar -> CalendarDate calendar

  Extract the calendar date component.

Totality: total
Visibility: public export

localTimeOfDay : {auto cal : Calendar calendar} -> CalendarDateTime calendar -> LocalTime

  Extract the local time-of-day component.

Totality: total
Visibility: public export

atDatePart : {auto cal : Calendar calendar} -> (valueDate : CalendarDate calendar) -> (valueTime : LocalTime) -> datePart (at valueDate valueTime) = valueDate

  Extracting the date after construction returns the supplied date.

Totality: total
Visibility: public export

atLocalTimeOfDay : {auto cal : Calendar calendar} -> (valueDate : CalendarDate calendar) -> (valueTime : LocalTime) -> localTimeOfDay (at valueDate valueTime) = valueTime

  Extracting the local time after construction returns the supplied time.

Totality: total
Visibility: public export

calendarDateTimeRoundTrip : {auto cal : Calendar calendar} -> (value : CalendarDateTime calendar) -> at (datePart value) (localTimeOfDay value) = value

  Reconstructing a calendar date-time from its projections is exact.

Totality: total
Visibility: public export

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

  Convert the date component to another calendar through their shared bridge
  day while preserving the local time of day.

Totality: total
Visibility: public export

between : {auto cal : Calendar calendar} -> CalendarDateTime calendar -> CalendarDateTime calendar -> Period (CalendarDateTime calendar)

  Compute the exact signed period from `start` to `end`, treating each civil
  calendar day as 24 hours.

Totality: total
Visibility: public export