IotaTime.Duration

Definitions

record DurationRep : Type

  A fixed amount of elapsed timeline time, measured in nanoseconds.
  Unlike `Period`, a duration has no calendar-relative units.

Totality: total
Visibility: export
Constructor: 

MkDuration : Integer -> DurationRep

Projection: 

.storedNanoseconds : DurationRep -> Integer

Duration : Type

  The public opaque type of fixed elapsed durations.

Totality: total
Visibility: public export

durationFromNanoseconds : Integer -> Duration

  Construct a duration from an exact number of nanoseconds.

Totality: total
Visibility: export

fromNanoseconds : Integer -> Duration

  Construct a duration from an exact number of nanoseconds.

Totality: total
Visibility: public export

durationFromMicroseconds : Integer -> Duration

  Construct a duration from an exact number of microseconds.

Totality: total
Visibility: export

fromMicroseconds : Integer -> Duration

  Construct a duration from an exact number of microseconds.

Totality: total
Visibility: public export

durationFromMilliseconds : Integer -> Duration

  Construct a duration from an exact number of milliseconds.

Totality: total
Visibility: export

fromMilliseconds : Integer -> Duration

  Construct a duration from an exact number of milliseconds.

Totality: total
Visibility: public export

durationFromSeconds : Integer -> Duration

  Construct a duration from an exact number of seconds.

Totality: total
Visibility: export

fromSeconds : Integer -> Duration

  Construct a duration from an exact number of seconds.

Totality: total
Visibility: public export

durationFromMinutes : Integer -> Duration

  Construct a duration from fixed 60-second minutes.

Totality: total
Visibility: export

fromMinutes : Integer -> Duration

  Construct a duration from fixed 60-second minutes.

Totality: total
Visibility: public export

durationFromHours : Integer -> Duration

  Construct a duration from fixed 60-minute hours.

Totality: total
Visibility: export

fromHours : Integer -> Duration

  Construct a duration from fixed 60-minute hours.

Totality: total
Visibility: public export

durationFromStandardDays : Integer -> Duration

  Construct a duration from fixed 24-hour days, independent of calendars and zones.

Totality: total
Visibility: export

fromStandardDays : Integer -> Duration

  Construct a duration from fixed 24-hour days, independent of calendars and zones.

Totality: total
Visibility: public export

durationFromStandardWeeks : Integer -> Duration

  Construct a duration from fixed seven-day weeks.

Totality: total
Visibility: export

fromStandardWeeks : Integer -> Duration

  Construct a duration from fixed seven-day weeks.

Totality: total
Visibility: public export

toDurationNanoseconds : Duration -> Integer

  Return the exact signed nanosecond count represented by a duration.

Totality: total
Visibility: public export

toMicroseconds : Duration -> Integer

  Return the number of whole microseconds in a duration.

Totality: total
Visibility: public export

toMilliseconds : Duration -> Integer

  Return the number of whole milliseconds in a duration.

Totality: total
Visibility: public export

toSeconds : Duration -> Integer

  Return the number of whole seconds in a duration, truncated toward negative infinity.

Totality: total
Visibility: public export

toMinutes : Duration -> Integer

  Return the number of whole fixed 60-second minutes in a duration.

Totality: total
Visibility: public export

toHours : Duration -> Integer

  Return the number of whole fixed 60-minute hours in a duration.

Totality: total
Visibility: public export

toStandardDays : Duration -> Integer

  Return the number of whole fixed 24-hour days in a duration.

Totality: total
Visibility: public export

toStandardWeeks : Duration -> Integer

  Return the number of whole fixed seven-day weeks in a duration.

Totality: total
Visibility: public export

zeroDuration : Duration

  The duration containing no elapsed time.

Totality: total
Visibility: export

addDurations : Duration -> Duration -> Duration

  Add two elapsed durations.

Totality: total
Visibility: export

add : Duration -> Duration -> Duration

  Add two elapsed durations.

Totality: total
Visibility: public export

subtractDurations : Duration -> Duration -> Duration

  Subtract the second duration from the first.

Totality: total
Visibility: export

minus : Duration -> Duration -> Duration

  Subtract the second duration from the first.

Totality: total
Visibility: public export

negateDuration : Duration -> Duration

  Reverse the direction of a duration.

Totality: total
Visibility: export

scaleDuration : Integer -> Duration -> Duration

  Multiply a duration by an integer factor.

Totality: total
Visibility: export

durationNanosecondsRoundTrip : (value : Integer) -> toDurationNanoseconds (fromNanoseconds value) = value

  Proof that constructing then observing a nanosecond count is lossless.

Totality: total
Visibility: public export

durationRoundTrip : (value : Duration) -> fromNanoseconds (toDurationNanoseconds value) = value

  Proof that observing then reconstructing a duration preserves it.

Totality: total
Visibility: public export