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

Equations

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

@[implicit_reducible]

instance Std.Time.instReprWallTime : Repr WallTime

Equations

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

@[implicit_reducible]

instance Std.Time.instDecidableEqWallTime : DecidableEq WallTime

Equations

• Std.Time.instDecidableEqWallTime = Std.Time.instDecidableEqWallTime.decEq

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

Equations

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

@[implicit_reducible]

instance Std.Time.instInhabitedWallTime : Inhabited WallTime

Equations

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

@[implicit_reducible]

instance Std.Time.instLEWallTime : LE WallTime

Equations

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

@[implicit_reducible]

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

Equations

• Std.Time.instDecidableLeWallTime = Std.Time.Duration.instDecidableLe

@[implicit_reducible]

instance Std.Time.instLTWallTime : LT WallTime

Equations

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

@[implicit_reducible]

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

Equations

• Std.Time.instDecidableLtWallTime = Std.Time.Duration.instDecidableLt

@[implicit_reducible]

instance Std.Time.instOrdWallTime : Ord WallTime

Equations

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

@[implicit_reducible]

instance Std.Time.instToStringWallTime : ToString WallTime

Equations

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

@[implicit_reducible]

instance Std.Time.instReprWallTime_1 : Repr WallTime

Equations

• Std.Time.instReprWallTime_1 = { reprPrec := fun (s : Std.Time.WallTime) => Repr.addAppParen (Std.Format.text "WallTime.ofNanoseconds " ++ repr s.val.toNanoseconds) }

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

Equations

• Std.Time.WallTime.ofDuration duration = { val := duration }

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

Equations

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

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

Equations

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

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

Equations

• wt.toSeconds = wt.val.second

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

Equations

• wt.toNanoseconds = Std.Time.Internal.UnitVal.mul wt.toSeconds 1000000000 + { val := wt.val.nano.val }

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

Equations

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

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

Equations

• tm.toDays = tm.val.second.toDays

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

Equations

• Std.Time.WallTime.ofMilliseconds milli = { val := Std.Time.Duration.ofNanoseconds milli.toNanoseconds }

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

Equations

• tm.toMilliseconds = tm.toNanoseconds.toMilliseconds

@[inline]

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

Adds a Millisecond.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Millisecond.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds a Nanosecond.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Nanosecond.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds a Second.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Second.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds a Minute.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Minute.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds an Hour.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts an Hour.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds a Day.Offset to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Day.Offset from the given WallTime.

Equations

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

@[inline]

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

Adds a Week.Offset to the given WallTime.

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.WallTime.subWeeks (t : WallTime) (d : Week.Offset) : WallTime

Subtracts a Week.Offset from the given WallTime.

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.WallTime.addDuration (t : WallTime) (d : Duration) : WallTime

Adds a Duration to the given WallTime.

Equations

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

@[inline]

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

Subtracts a Duration from the given WallTime.

Equations

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

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

Equations

• wt.toDuration = wt.val

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Std.Time.WallTime.instOfNat = { ofNat := Std.Time.WallTime.ofSeconds (Std.Time.Second.Offset.ofNat n) }