source
structure Std.Time.Timestamp :
Type

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

- val : Duration

  Duration since the unix epoch.

Instances For

source
theorem Std.Time.Timestamp.ext_iff {x y : Timestamp} :
x = y ↔ x.val = y.val
source
theorem Std.Time.Timestamp.ext {x y : Timestamp} (val : x.val = y.val) :
x = y
source
def Std.Time.instReprTimestamp.repr :
Timestamp → Nat → Std.Format
Equations

- Std.Time.instReprTimestamp.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "val" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.val)).group) " }"

Instances For

source
instance Std.Time.instReprTimestamp :
Repr Timestamp
Equations

- Std.Time.instReprTimestamp = { reprPrec := Std.Time.instReprTimestamp.repr }

source
instance Std.Time.instDecidableEqTimestamp :
DecidableEq Timestamp
Equations

- Std.Time.instDecidableEqTimestamp = Std.Time.instDecidableEqTimestamp.decEq

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

- Std.Time.instDecidableEqTimestamp.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source
instance Std.Time.instInhabitedTimestamp :
Inhabited Timestamp
Equations

- Std.Time.instInhabitedTimestamp = { default := Std.Time.instInhabitedTimestamp.default }

source
def Std.Time.instInhabitedTimestamp.default :
Timestamp
Equations

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

Instances For

source
instance Std.Time.instLETimestamp :
LE Timestamp
Equations

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

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

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

source
instance Std.Time.instLTTimestamp :
LT Timestamp
Equations

- Std.Time.instLTTimestamp = { lt := fun (x y : Std.Time.Timestamp) => x.val < y.val }

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

- Std.Time.instDecidableLtTimestamp = inferInstanceAs (Decidable (x.val < y.val))

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

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

source
instance Std.Time.instToStringTimestamp :
ToString Timestamp
Equations

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

source
instance Std.Time.instReprTimestamp_1 :
Repr Timestamp
Equations

- Std.Time.instReprTimestamp_1 = { reprPrec := fun (s : Std.Time.Timestamp) => Repr.addAppParen (Std.Format.text "Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds) }

source
instance Std.Time.instOrdTimestamp :
Ord Timestamp
Equations

- Std.Time.instOrdTimestamp = { compare := compareOn fun (x : Std.Time.Timestamp) => x.val }

source
theorem Std.Time.Timestamp.compare_def :
compare = compareOn fun (x : Timestamp) => x.val
source
instance Std.Time.instTransOrdTimestamp :
TransOrd Timestamp
source
instance Std.Time.instLawfulEqOrdTimestamp :
LawfulEqOrd Timestamp
source
@[extern lean_get_current_time]
opaque Std.Time.Timestamp.now :
IO Timestamp

Fetches the current duration from the system.

source
@[inline]
def Std.Time.Timestamp.toMinutes (tm : Timestamp) :
Minute.Offset

Converts a `Timestamp` to minutes as `Minute.Offset`.

Equations

- tm.toMinutes = tm.val.second.toMinutes

Instances For

source
@[inline]
def Std.Time.Timestamp.toDays (tm : Timestamp) :
Day.Offset

Converts a `Timestamp` to days as `Day.Offset`.

Equations

- tm.toDays = tm.val.second.toDays

Instances For

source
@[inline]
def Std.Time.Timestamp.ofSecondsSinceUnixEpoch (secs : Second.Offset) :
Timestamp

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

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.ofNanosecondsSinceUnixEpoch (nanos : Nanosecond.Offset) :
Timestamp

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

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.ofMillisecondsSinceUnixEpoch (milli : Millisecond.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.toSecondsSinceUnixEpoch (t : Timestamp) :
Second.Offset

Converts a `Timestamp` to seconds as `Second.Offset`.

Equations

- t.toSecondsSinceUnixEpoch = t.val.second

Instances For

source
@[inline]
def Std.Time.Timestamp.toNanosecondsSinceUnixEpoch (tm : Timestamp) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.toMillisecondsSinceUnixEpoch (tm : Timestamp) :
Millisecond.Offset

Converts a `Timestamp` to nanoseconds as `Millisecond.Offset`.

Equations

- tm.toMillisecondsSinceUnixEpoch = tm.toNanosecondsSinceUnixEpoch.toMilliseconds

Instances For

source
@[inline]
def Std.Time.Timestamp.since (f : Timestamp) :
IO 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)

Instances For

source
@[inline]
def Std.Time.Timestamp.toDurationSinceUnixEpoch (tm : Timestamp) :
Duration

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

Equations

- tm.toDurationSinceUnixEpoch = tm.val

Instances For

source
@[inline]
def Std.Time.Timestamp.addMilliseconds (t : Timestamp) (s : Millisecond.Offset) :
Timestamp

Adds a `Millisecond.Offset` to the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.subMilliseconds (t : Timestamp) (s : Millisecond.Offset) :
Timestamp

Subtracts a `Millisecond.Offset` from the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.addNanoseconds (t : Timestamp) (s : Nanosecond.Offset) :
Timestamp

Adds a `Nanosecond.Offset` to the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.subNanoseconds (t : Timestamp) (s : Nanosecond.Offset) :
Timestamp

Subtracts a `Nanosecond.Offset` from the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.addSeconds (t : Timestamp) (s : Second.Offset) :
Timestamp

Adds a `Second.Offset` to the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.subSeconds (t : Timestamp) (s : Second.Offset) :
Timestamp

Subtracts a `Second.Offset` from the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.addMinutes (t : Timestamp) (m : Minute.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.subMinutes (t : Timestamp) (m : Minute.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.addHours (t : Timestamp) (h : Hour.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.subHours (t : Timestamp) (h : Hour.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.addDays (t : Timestamp) (d : Day.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.subDays (t : Timestamp) (d : Day.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.addWeeks (t : Timestamp) (d : Week.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.subWeeks (t : Timestamp) (d : Week.Offset) :
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 }

Instances For

source
@[inline]
def Std.Time.Timestamp.addDuration (t : Timestamp) (d : Duration) :
Timestamp

Adds a `Duration` to the given `Timestamp`.

Equations

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

Instances For

source
@[inline]
def Std.Time.Timestamp.subDuration (t : Timestamp) (d : Duration) :
Timestamp

Subtracts a `Duration` from the given `Timestamp`.

Equations

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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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