structure Std.Time.Timestamp : Type

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

• val : Std.Time.Duration

  Duration since the unix epoch.

instance Std.Time.instReprTimestamp : Repr Std.Time.Timestamp

Equations

• Std.Time.instReprTimestamp = { reprPrec := Std.Time.reprTimestamp✝ }

instance Std.Time.instBEqTimestamp : BEq Std.Time.Timestamp

Equations

• Std.Time.instBEqTimestamp = { beq := Std.Time.beqTimestamp✝ }

instance Std.Time.instInhabitedTimestamp : Inhabited Std.Time.Timestamp

Equations

• Std.Time.instInhabitedTimestamp = { default := { val := default } }

instance Std.Time.instLETimestamp : LE Std.Time.Timestamp

Equations

• Std.Time.instLETimestamp = { le := fun (x y : Std.Time.Timestamp) => x.val ≤ y.val }

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

Equations

• Std.Time.instDecidableLeTimestamp = inferInstanceAs (Decidable (x.val ≤ y.val))

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

Equations

• Std.Time.instOfNatTimestamp = { ofNat := { val := OfNat.ofNat n } }

instance Std.Time.instToStringTimestamp : ToString Std.Time.Timestamp

Equations

• Std.Time.instToStringTimestamp = { toString := fun (s : Std.Time.Timestamp) => toString s.val.toMilliseconds }

instance Std.Time.instReprTimestamp_1 : Repr Std.Time.Timestamp

Equations

• Std.Time.instReprTimestamp_1 = { reprPrec := fun (s : Std.Time.Timestamp) => reprPrec (toString s) }

@[extern lean_get_current_time]

opaque Std.Time.Timestamp.now : IO Std.Time.Timestamp

Fetches the current duration from the system.

@[inline]

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

Converts a Timestamp to minutes as Minute.Offset.

Equations

• tm.toMinutes = Std.Time.Internal.UnitVal.ediv tm.val.second 60

@[inline]

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

Converts a Timestamp to days as Day.Offset.

Equations

• tm.toDays = Std.Time.Internal.UnitVal.ediv tm.val.second 86400

@[inline]

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

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

Equations

• Std.Time.Timestamp.ofSecondsSinceUnixEpoch secs = { val := Std.Time.Duration.ofSeconds secs }

@[inline]

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

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

Equations

• Std.Time.Timestamp.ofNanosecondsSinceUnixEpoch nanos = { val := Std.Time.Duration.ofNanoseconds nanos }

@[inline]

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

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

Equations

• Std.Time.Timestamp.ofMillisecondsSinceUnixEpoch milli = { val := Std.Time.Duration.ofNanoseconds milli.toNanoseconds }

@[inline]

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

Converts a Timestamp to seconds as Second.Offset.

Equations

• t.toSecondsSinceUnixEpoch = t.val.second

@[inline]

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

Converts a Timestamp to nanoseconds as Nanosecond.Offset.

Equations

• tm.toNanosecondsSinceUnixEpoch = Std.Time.Internal.UnitVal.mul tm.toSecondsSinceUnixEpoch 1000000000 + { val := tm.val.nano.val }

@[inline]

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

Converts a Timestamp to nanoseconds as Millisecond.Offset.

Equations

• tm.toMillisecondsSinceUnixEpoch = tm.toNanosecondsSinceUnixEpoch.toMilliseconds

@[inline]

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

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

Equations

• f.since = do let cur ← Std.Time.Timestamp.now pure (cur.val.sub f.val)

@[inline]

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

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

Equations

• tm.toDurationSinceUnixEpoch = tm.val

@[inline]

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

Adds a Millisecond.Offset to the given Timestamp.

Equations

• t.addMilliseconds s = { val := t.val + s }

@[inline]

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

Subtracts a Millisecond.Offset from the given Timestamp.

Equations

• t.subMilliseconds s = { val := t.val - s }

@[inline]

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

Adds a Nanosecond.Offset to the given Timestamp.

Equations

• t.addNanoseconds s = { val := t.val + Std.Time.Duration.ofNanoseconds s }

@[inline]

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

Subtracts a Nanosecond.Offset from the given Timestamp.

Equations

• t.subNanoseconds s = { val := t.val - Std.Time.Duration.ofNanoseconds s }

@[inline]

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

Adds a Second.Offset to the given Timestamp.

Equations

• t.addSeconds s = { val := t.val + Std.Time.Duration.ofSeconds s }

@[inline]

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

Subtracts a Second.Offset from the given Timestamp.

Equations

• t.subSeconds s = { val := t.val - Std.Time.Duration.ofSeconds s }

@[inline]

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

Adds a Minute.Offset to the given Timestamp.

Equations

• t.addMinutes m = { val := t.val + (Std.Time.Duration.ofSeconds ∘ Std.Time.Minute.Offset.toSeconds) m }

@[inline]

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

Subtracts a Minute.Offset from the given Timestamp.

Equations

• t.subMinutes m = { val := t.val - (Std.Time.Duration.ofSeconds ∘ Std.Time.Minute.Offset.toSeconds) m }

@[inline]

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

Adds an Hour.Offset to the given Timestamp.

Equations

• t.addHours h = { val := t.val + (Std.Time.Duration.ofSeconds ∘ Std.Time.Hour.Offset.toSeconds) h }

@[inline]

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

Subtracts an Hour.Offset from the given Timestamp.

Equations

• t.subHours h = { val := t.val - (Std.Time.Duration.ofSeconds ∘ Std.Time.Hour.Offset.toSeconds) h }

@[inline]

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

Adds a Day.Offset to the given Timestamp.

Equations

• t.addDays d = { val := t.val + (Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds) d }

@[inline]

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

Subtracts a Day.Offset from the given Timestamp.

Equations

• t.subDays d = { val := t.val - (Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds) d }

@[inline]

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

Adds a Week.Offset to the given Timestamp.

Equations

• t.addWeeks d = { val := t.val + (Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds ∘ Std.Time.Week.Offset.toDays) d }

@[inline]

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

Subtracts a Week.Offset from the given Timestamp.

Equations

• t.subWeeks d = { val := t.val - (Std.Time.Duration.ofSeconds ∘ Std.Time.Day.Offset.toSeconds ∘ Std.Time.Week.Offset.toDays) d }

@[inline]

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

Adds a Duration to the given Timestamp.

Equations

• t.addDuration d = { val := t.val + d }

@[inline]

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

Subtracts a Duration from the given Timestamp.

Equations

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

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

Equations

• Std.Time.Timestamp.instHAddDuration = { hAdd := Std.Time.Timestamp.addDuration }

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

Equations

• Std.Time.Timestamp.instHSubDuration = { hSub := Std.Time.Timestamp.subDuration }

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

Equations

• Std.Time.Timestamp.instHAddOffset = { hAdd := Std.Time.Timestamp.addDays }

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

Equations

• Std.Time.Timestamp.instHSubOffset = { hSub := Std.Time.Timestamp.subDays }

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

Equations

• Std.Time.Timestamp.instHAddOffset_1 = { hAdd := Std.Time.Timestamp.addWeeks }

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

Equations

• Std.Time.Timestamp.instHSubOffset_1 = { hSub := Std.Time.Timestamp.subWeeks }

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

Equations

• Std.Time.Timestamp.instHAddOffset_2 = { hAdd := Std.Time.Timestamp.addHours }

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

Equations

• Std.Time.Timestamp.instHSubOffset_2 = { hSub := Std.Time.Timestamp.subHours }

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

Equations

• Std.Time.Timestamp.instHAddOffset_3 = { hAdd := Std.Time.Timestamp.addMinutes }

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

Equations

• Std.Time.Timestamp.instHSubOffset_3 = { hSub := Std.Time.Timestamp.subMinutes }

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

Equations

• Std.Time.Timestamp.instHAddOffset_4 = { hAdd := Std.Time.Timestamp.addSeconds }

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

Equations

• Std.Time.Timestamp.instHSubOffset_4 = { hSub := Std.Time.Timestamp.subSeconds }

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

Equations

• Std.Time.Timestamp.instHAddOffset_5 = { hAdd := Std.Time.Timestamp.addMilliseconds }

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

Equations

• Std.Time.Timestamp.instHSubOffset_5 = { hSub := Std.Time.Timestamp.subMilliseconds }

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

Equations

• Std.Time.Timestamp.instHAddOffset_6 = { hAdd := Std.Time.Timestamp.addNanoseconds }

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

Equations

• Std.Time.Timestamp.instHSubOffset_6 = { hSub := Std.Time.Timestamp.subNanoseconds }

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

Equations

• Std.Time.Timestamp.instHSubDuration_1 = { hSub := fun (x y : Std.Time.Timestamp) => x.val - y.val }