IotaTime.Instant

Definitions

record Instant : Type

  A fixed point on the global timeline, measured in nanoseconds from
  March 1, 2000 at 00:00:00 UTC.
  
  Representation benchmark note: if profiling shows scalar `Integer`
  arithmetic to be costly, compare it with a proof-oriented record of an
  `Integer` day, `Fin 86400` second-of-day, and `Fin 1000000000` nanosecond.
  The scalar is preferred until then because canonical form is structural
  and arithmetic cannot overflow or require normalization proofs.

Totality: total
Visibility: export
Constructor: 

MkInstant : Integer -> Instant

Projection: 

.storedNanoseconds : Instant -> Integer

Hints:

Eq Instant

Ord Instant

Show Instant

fromNanosecondsSinceEpoch : Integer -> Instant

  Construct an instant from nanoseconds relative to the library epoch.

Totality: total
Visibility: public export

toNanosecondsSinceEpoch : Instant -> Integer

  Read an instant as nanoseconds relative to the library epoch.

Totality: total
Visibility: public export

ticks : Instant -> Integer

  Backward-compatible name for `toNanosecondsSinceEpoch`.

Totality: total
Visibility: export

instantNanosecondsRoundTrip : (value : Integer) -> toNanosecondsSinceEpoch (fromNanosecondsSinceEpoch value) = value

  Converting a scalar nanosecond count to an instant and back is exact.

Totality: total
Visibility: public export

instantRoundTrip : (value : Instant) -> fromNanosecondsSinceEpoch (toNanosecondsSinceEpoch value) = value

  Reconstructing an instant from its scalar nanosecond count is exact.

Totality: total
Visibility: public export

fromSecondsSinceUnixEpoch : Integer -> Instant

  Construct an instant from whole seconds relative to the Unix epoch.

Totality: total
Visibility: public export

fromNanosecondsSinceUnixEpoch : Integer -> Instant

  Construct an instant from nanoseconds relative to the Unix epoch.

Totality: total
Visibility: public export

toNanosecondsSinceUnixEpoch : Instant -> Integer

  Read an instant as nanoseconds relative to the Unix epoch.

Totality: total
Visibility: public export

toSecondsSinceUnixEpoch : Instant -> Integer

  Read an instant as whole seconds relative to the Unix epoch, truncated toward negative infinity.

Totality: total
Visibility: public export

addDuration : Instant -> Duration -> Instant

  Add a fixed duration to an instant.

Totality: total
Visibility: export

add : Instant -> Duration -> Instant

Totality: total
Visibility: public export

subtractDuration : Instant -> Duration -> Instant

  Subtract a fixed duration from an instant.

Totality: total
Visibility: export

minus : Instant -> Duration -> Instant

Totality: total
Visibility: public export

difference : Instant -> Instant -> Duration

  Compute the signed fixed duration from the second instant to the first.

Totality: total
Visibility: public export

now : IO Instant

  Read the current UTC system clock as an instant.

Totality: total
Visibility: public export

epoch : Instant

  The library epoch: March 1, 2000 at 00:00:00 UTC.

Totality: total
Visibility: public export