structure Std.Time.Timestamp : Type

Represents an exact point in time as a UNIX Epoch timestamp.

• val : Duration

  Duration since the unix epoch.

theorem Std.Time.Timestamp.ext_iff {x y : Timestamp} : x = y ↔ x.val = y.val

theorem Std.Time.Timestamp.ext {x y : Timestamp} (val : x.val = y.val) : x = y

def Std.Time.instReprTimestamp.repr : Timestamp → Nat → Std.Format

instance Std.Time.instReprTimestamp : Repr Timestamp

instance Std.Time.instDecidableEqTimestamp : DecidableEq Timestamp

def Std.Time.instDecidableEqTimestamp.decEq (x✝ x✝¹ : Timestamp) : Decidable (x✝ = x✝¹)

instance Std.Time.instInhabitedTimestamp : Inhabited Timestamp

def Std.Time.instInhabitedTimestamp.default : Timestamp

instance Std.Time.instLETimestamp : LE Timestamp

instance Std.Time.instDecidableLeTimestamp {x y : Timestamp} : Decidable (x ≤ y)

instance Std.Time.instLTTimestamp : LT Timestamp

instance Std.Time.instDecidableLtTimestamp {x y : Timestamp} : Decidable (x < y)

instance Std.Time.instOfNatTimestamp {n : Nat} : OfNat Timestamp n

instance Std.Time.instToStringTimestamp : ToString Timestamp

instance Std.Time.instReprTimestamp_1 : Repr Timestamp

instance Std.Time.instOrdTimestamp : Ord Timestamp

theorem Std.Time.Timestamp.compare_def : compare = compareOn fun (x : Timestamp) => x.val

instance Std.Time.instTransOrdTimestamp : TransOrd Timestamp

instance Std.Time.instLawfulEqOrdTimestamp : LawfulEqOrd Timestamp

@[extern lean_get_current_time]

opaque Std.Time.Timestamp.now : IO Timestamp

Fetches the current duration from the system.

@[inline]

def Std.Time.Timestamp.toMinutes (tm : Timestamp) : Minute.Offset

Converts a Timestamp to minutes as Minute.Offset.

@[inline]

def Std.Time.Timestamp.toDays (tm : Timestamp) : Day.Offset

Converts a Timestamp to days as Day.Offset.

@[inline]

def Std.Time.Timestamp.ofSecondsSinceUnixEpoch (secs : Second.Offset) : Timestamp

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

@[inline]

def Std.Time.Timestamp.ofNanosecondsSinceUnixEpoch (nanos : Nanosecond.Offset) : Timestamp

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

@[inline]

def Std.Time.Timestamp.ofMillisecondsSinceUnixEpoch (milli : Millisecond.Offset) : Timestamp

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

@[inline]

def Std.Time.Timestamp.toSecondsSinceUnixEpoch (t : Timestamp) : Second.Offset

Converts a Timestamp to seconds as Second.Offset.

@[inline]

def Std.Time.Timestamp.toNanosecondsSinceUnixEpoch (tm : Timestamp) : Nanosecond.Offset

Converts a Timestamp to nanoseconds as Nanosecond.Offset.

@[inline]

def Std.Time.Timestamp.toMillisecondsSinceUnixEpoch (tm : Timestamp) : Millisecond.Offset

Converts a Timestamp to nanoseconds as Millisecond.Offset.

@[inline]

def Std.Time.Timestamp.since (f : Timestamp) : IO Duration

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

@[inline]

def Std.Time.Timestamp.toDurationSinceUnixEpoch (tm : Timestamp) : Duration

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

@[inline]

def Std.Time.Timestamp.addMilliseconds (t : Timestamp) (s : Millisecond.Offset) : Timestamp

Adds a Millisecond.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subMilliseconds (t : Timestamp) (s : Millisecond.Offset) : Timestamp

Subtracts a Millisecond.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addNanoseconds (t : Timestamp) (s : Nanosecond.Offset) : Timestamp

Adds a Nanosecond.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subNanoseconds (t : Timestamp) (s : Nanosecond.Offset) : Timestamp

Subtracts a Nanosecond.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addSeconds (t : Timestamp) (s : Second.Offset) : Timestamp

Adds a Second.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subSeconds (t : Timestamp) (s : Second.Offset) : Timestamp

Subtracts a Second.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addMinutes (t : Timestamp) (m : Minute.Offset) : Timestamp

Adds a Minute.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subMinutes (t : Timestamp) (m : Minute.Offset) : Timestamp

Subtracts a Minute.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addHours (t : Timestamp) (h : Hour.Offset) : Timestamp

Adds an Hour.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subHours (t : Timestamp) (h : Hour.Offset) : Timestamp

Subtracts an Hour.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addDays (t : Timestamp) (d : Day.Offset) : Timestamp

Adds a Day.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subDays (t : Timestamp) (d : Day.Offset) : Timestamp

Subtracts a Day.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addWeeks (t : Timestamp) (d : Week.Offset) : Timestamp

Adds a Week.Offset to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subWeeks (t : Timestamp) (d : Week.Offset) : Timestamp

Subtracts a Week.Offset from the given Timestamp.

@[inline]

def Std.Time.Timestamp.addDuration (t : Timestamp) (d : Duration) : Timestamp

Adds a Duration to the given Timestamp.

@[inline]

def Std.Time.Timestamp.subDuration (t : Timestamp) (d : Duration) : Timestamp

Subtracts a Duration from the given Timestamp.

instance Std.Time.Timestamp.instHAddDuration : HAdd Timestamp Duration Timestamp

instance Std.Time.Timestamp.instHSubDuration : HSub Timestamp Duration Timestamp

instance Std.Time.Timestamp.instHAddOffset : HAdd Timestamp Day.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset : HSub Timestamp Day.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_1 : HAdd Timestamp Week.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_1 : HSub Timestamp Week.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_2 : HAdd Timestamp Hour.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_2 : HSub Timestamp Hour.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_3 : HAdd Timestamp Minute.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_3 : HSub Timestamp Minute.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_4 : HAdd Timestamp Second.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_4 : HSub Timestamp Second.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_5 : HAdd Timestamp Millisecond.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_5 : HSub Timestamp Millisecond.Offset Timestamp

instance Std.Time.Timestamp.instHAddOffset_6 : HAdd Timestamp Nanosecond.Offset Timestamp

instance Std.Time.Timestamp.instHSubOffset_6 : HSub Timestamp Nanosecond.Offset Timestamp

instance Std.Time.Timestamp.instHSubDuration_1 : HSub Timestamp Timestamp Duration