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

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) " }"

instance Std.Time.instReprTimestamp : Repr Timestamp

Equations

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

instance Std.Time.instDecidableEqTimestamp : DecidableEq Timestamp

Equations

• Std.Time.instDecidableEqTimestamp = Std.Time.instDecidableEqTimestamp.decEq

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 ⋯

instance Std.Time.instInhabitedTimestamp : Inhabited Timestamp

Equations

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

def Std.Time.instInhabitedTimestamp.default : Timestamp

Equations

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

instance Std.Time.instLETimestamp : LE Timestamp

Equations

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

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

Equations

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

instance Std.Time.instLTTimestamp : LT Timestamp

Equations

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

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

Equations

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

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

Equations

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

instance Std.Time.instToStringTimestamp : ToString Timestamp

Equations

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

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) }

instance Std.Time.instOrdTimestamp : Ord Timestamp

Equations

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

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.

Equations

• tm.toMinutes = tm.val.second.toMinutes

@[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

@[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 }

@[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 }

@[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 }

@[inline]

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

Converts a Timestamp to seconds as Second.Offset.

Equations

• t.toSecondsSinceUnixEpoch = t.val.second

@[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 }

@[inline]

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

Converts a Timestamp to nanoseconds as Millisecond.Offset.

Equations

• tm.toMillisecondsSinceUnixEpoch = tm.toNanosecondsSinceUnixEpoch.toMilliseconds

@[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)

@[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

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

@[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 }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 }