structure Std.Time.WallTime : Type

A wall-clock time is what a clock shows in a given timezone: the local civil time at some point in time. It is stored as a Duration since 1970-01-01T00:00:00 in local time, equivalent to a PlainDateTime packed into a single offset, which makes arithmetic straightforward.

Every timezone induces a correspondence between Timestamp and WallTime: interpreting a Timestamp in a timezone yields the WallTime (what a clock in that timezone reads at that instant), and resolving a WallTime in a timezone yields the Timestamp (the absolute instant the clock reading refers to).

• val : Duration

  Duration since 1970-01-01T00:00:00 in local (civil) time.

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

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

def Std.Time.instReprWallTime.repr : WallTime → Nat → Std.Format

@[implicit_reducible]

instance Std.Time.instReprWallTime : Repr WallTime

@[implicit_reducible]

instance Std.Time.instDecidableEqWallTime : DecidableEq WallTime

def Std.Time.instDecidableEqWallTime.decEq (x✝ x✝¹ : WallTime) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Time.instInhabitedWallTime : Inhabited WallTime

@[implicit_reducible]

instance Std.Time.instLEWallTime : LE WallTime

@[implicit_reducible]

instance Std.Time.instDecidableLeWallTime {x y : WallTime} : Decidable (x ≤ y)

@[implicit_reducible]

instance Std.Time.instLTWallTime : LT WallTime

@[implicit_reducible]

instance Std.Time.instDecidableLtWallTime {x y : WallTime} : Decidable (x < y)

@[implicit_reducible]

instance Std.Time.instOrdWallTime : Ord WallTime

@[implicit_reducible]

instance Std.Time.instToStringWallTime : ToString WallTime

@[implicit_reducible]

instance Std.Time.instReprWallTime_1 : Repr WallTime

@[inline]

def Std.Time.WallTime.ofDuration (duration : Duration) : WallTime

Creates a WallTime from a Duration. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.ofSeconds (secs : Second.Offset) : WallTime

Creates a WallTime from a Second.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.ofNanoseconds (nanos : Nanosecond.Offset) : WallTime

Creates a WallTime from a Nanosecond.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.toSeconds (wt : WallTime) : Second.Offset

Converts a WallTime to a Second.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.toNanoseconds (wt : WallTime) : Nanosecond.Offset

Converts a WallTime to a Nanosecond.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

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

Converts a WallTime to a Minute.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

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

Converts a WallTime to a Day.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.ofMilliseconds (milli : Millisecond.Offset) : WallTime

Creates a WallTime from a Millisecond.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

def Std.Time.WallTime.toMilliseconds (tm : WallTime) : Millisecond.Offset

Converts a WallTime to a Millisecond.Offset. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[inline]

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

Adds a Millisecond.Offset to the given WallTime.

@[inline]

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

Subtracts a Millisecond.Offset from the given WallTime.

@[inline]

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

Adds a Nanosecond.Offset to the given WallTime.

@[inline]

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

Subtracts a Nanosecond.Offset from the given WallTime.

@[inline]

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

Adds a Second.Offset to the given WallTime.

@[inline]

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

Subtracts a Second.Offset from the given WallTime.

@[inline]

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

Adds a Minute.Offset to the given WallTime.

@[inline]

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

Subtracts a Minute.Offset from the given WallTime.

@[inline]

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

Adds an Hour.Offset to the given WallTime.

@[inline]

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

Subtracts an Hour.Offset from the given WallTime.

@[inline]

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

Adds a Day.Offset to the given WallTime.

@[inline]

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

Subtracts a Day.Offset from the given WallTime.

@[inline]

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

Adds a Week.Offset to the given WallTime.

@[inline]

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

Subtracts a Week.Offset from the given WallTime.

@[inline]

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

Adds a Duration to the given WallTime.

@[inline]

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

Subtracts a Duration from the given WallTime.

@[inline]

def Std.Time.WallTime.toDuration (wt : WallTime) : Duration

Converts a WallTime to a Duration. The epoch is 1970-01-01 00:00:00 in local (civil) time, not UTC.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Std.Time.WallTime.instOfNat {n : Nat} : OfNat WallTime n