Documentation

Std.Time.DateTime.Timestamp

Equations
Equations
@[extern lean_get_current_time]

Fetches the current duration from the system.

@[inline]

Converts a Timestamp to minutes as Minute.Offset.

Equations
@[inline]

Converts a Timestamp to days as Day.Offset.

Equations
@[inline]

Creates a Timestamp from a Second.Offset since the Unix epoch.

Equations
@[inline]

Creates a Timestamp from a Nanosecond.Offset since the Unix epoch.

Equations
@[inline]

Creates a Timestamp from a Millisecond.Offset since the Unix epoch.

Equations
@[inline]

Converts a Timestamp to seconds as Second.Offset.

Equations
  • t.toSecondsSinceUnixEpoch = t.val.second
@[inline]

Converts a Timestamp to nanoseconds as Nanosecond.Offset.

Equations
@[inline]

Converts a Timestamp to nanoseconds as Millisecond.Offset.

Equations
  • tm.toMillisecondsSinceUnixEpoch = tm.toNanosecondsSinceUnixEpoch.toMilliseconds
@[inline]

Calculates the duration from the given Timestamp to the current time.

Equations
@[inline]

Returns the Duration represented by the Timestamp since the Unix epoch.

Equations
  • tm.toDurationSinceUnixEpoch = tm.val
@[inline]

Adds a Millisecond.Offset to the given Timestamp.

Equations
  • t.addMilliseconds s = { val := t.val + s }
@[inline]

Subtracts a Millisecond.Offset from the given Timestamp.

Equations
  • t.subMilliseconds s = { val := t.val - s }
@[inline]

Adds a Nanosecond.Offset to the given Timestamp.

Equations
@[inline]

Subtracts a Nanosecond.Offset from the given Timestamp.

Equations
@[inline]

Adds a Second.Offset to the given Timestamp.

Equations
@[inline]

Subtracts a Second.Offset from the given Timestamp.

Equations
@[inline]

Adds a Minute.Offset to the given Timestamp.

Equations
@[inline]

Subtracts a Minute.Offset from the given Timestamp.

Equations
@[inline]

Adds an Hour.Offset to the given Timestamp.

Equations
@[inline]

Subtracts an Hour.Offset from the given Timestamp.

Equations
@[inline]

Adds a Day.Offset to the given Timestamp.

Equations
@[inline]

Subtracts a Day.Offset from the given Timestamp.

Equations
@[inline]

Adds a Week.Offset to the given Timestamp.

Equations
@[inline]

Subtracts a Week.Offset from the given Timestamp.

Equations
@[inline]

Adds a Duration to the given Timestamp.

Equations
  • t.addDuration d = { val := t.val + d }
@[inline]

Subtracts a Duration from the given Timestamp.

Equations
  • t.subDuration d = { val := t.val - d }