inductive Std.Time.TimeZone.UTLocal : Type

Represents the type of local time in relation to UTC.

• ut : UTLocal

  Universal Time (UT), often referred to as UTC.

• local : UTLocal

  Local time that is not necessarily UTC.

def Std.Time.TimeZone.instReprUTLocal.repr : UTLocal → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.TimeZone.instReprUTLocal : Repr UTLocal

Equations

• Std.Time.TimeZone.instReprUTLocal = { reprPrec := Std.Time.TimeZone.instReprUTLocal.repr }

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedUTLocal : Inhabited UTLocal

Equations

• Std.Time.TimeZone.instInhabitedUTLocal = { default := Std.Time.TimeZone.instInhabitedUTLocal.default }

inductive Std.Time.TimeZone.StdWall : Type

Represents types of wall clocks or standard times.

• wall : StdWall

  Time based on a wall clock, which can include daylight saving adjustments.

• standard : StdWall

  Standard time without adjustments for daylight saving.

@[implicit_reducible]

instance Std.Time.TimeZone.instReprStdWall : Repr StdWall

Equations

• Std.Time.TimeZone.instReprStdWall = { reprPrec := Std.Time.TimeZone.instReprStdWall.repr }

def Std.Time.TimeZone.instReprStdWall.repr : StdWall → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedStdWall : Inhabited StdWall

Equations

• Std.Time.TimeZone.instInhabitedStdWall = { default := Std.Time.TimeZone.instInhabitedStdWall.default }

structure Std.Time.TimeZone.LocalTimeType : Type

Represents a type of local time, including offset and daylight saving information.

• gmtOffset : Offset

  The offset from GMT for this local time.

• isDst : Bool

  Indicates if daylight saving time is observed.

• abbreviation : String

  The abbreviation for this local time type (e.g., "EST", "PDT").

• wall : StdWall

  Indicates if the time is wall clock or standard time.

• utLocal : UTLocal

  Distinguishes between universal time and local time.

• identifier : String

  ID of the timezone

@[implicit_reducible]

instance Std.Time.TimeZone.instReprLocalTimeType : Repr LocalTimeType

Equations

• Std.Time.TimeZone.instReprLocalTimeType = { reprPrec := Std.Time.TimeZone.instReprLocalTimeType.repr }

def Std.Time.TimeZone.instReprLocalTimeType.repr : LocalTimeType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedLocalTimeType : Inhabited LocalTimeType

Equations

• Std.Time.TimeZone.instInhabitedLocalTimeType = { default := Std.Time.TimeZone.instInhabitedLocalTimeType.default }

def Std.Time.TimeZone.LocalTimeType.getTimeZone (time : LocalTimeType) : TimeZone

Gets the TimeZone offset from a LocalTimeType.

Equations

• time.getTimeZone = { offset := time.gmtOffset, name := time.identifier, abbreviation := time.abbreviation, isDST := time.isDst }

structure Std.Time.TimeZone.Transition : Type

Represents a time zone transition, mapping a time to a local time type.

• time : Second.Offset

  The specific time of the transition event.

• localTimeType : LocalTimeType

  The local time type associated with this transition.

def Std.Time.TimeZone.instReprTransition.repr : Transition → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.TimeZone.instReprTransition : Repr Transition

Equations

• Std.Time.TimeZone.instReprTransition = { reprPrec := Std.Time.TimeZone.instReprTransition.repr }

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedTransition : Inhabited Transition

Equations

• Std.Time.TimeZone.instInhabitedTransition = { default := Std.Time.TimeZone.instInhabitedTransition.default }

structure Std.Time.TimeZone.ZoneRules : Type

Represents the rules for a time zone.

• initialLocalTimeType : LocalTimeType

  The first LocalTimeType used as a fallback when no matching transition is found.

• transitions : Array Transition

  The array of transitions for the time zone.

@[implicit_reducible]

instance Std.Time.TimeZone.instReprZoneRules : Repr ZoneRules

Equations

• Std.Time.TimeZone.instReprZoneRules = { reprPrec := Std.Time.TimeZone.instReprZoneRules.repr }

def Std.Time.TimeZone.instReprZoneRules.repr : ZoneRules → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedZoneRules : Inhabited ZoneRules

Equations

• Std.Time.TimeZone.instInhabitedZoneRules = { default := Std.Time.TimeZone.instInhabitedZoneRules.default }

def Std.Time.TimeZone.Transition.timestamp (t : Transition) : Timestamp

Returns the transition time as a Timestamp.

Equations

• t.timestamp = Std.Time.Timestamp.ofSecondsSinceUnixEpoch t.time

def Std.Time.TimeZone.Transition.createTimeZoneFromTransition (transition : Transition) : TimeZone

Create a TimeZone from a Transition.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.Transition.apply (timestamp : Timestamp) (transition : Transition) : Timestamp

Applies the transition to a Timestamp.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.Transition.findTransitionIndexForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Nat

Finds the transition corresponding to a given timestamp in Array Transition. If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.Transition.findTransitionForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Transition

Finds the transition corresponding to a given timestamp in Array Transition. If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.Transition.timezoneAt (transitions : Array Transition) (tm : Timestamp) : Except String TimeZone

Find the current TimeZone out of a Transition in a Array Transition

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.ZoneRules.fixedOffsetZone (second : Second.Offset) (identifier abbreviation : Option String := none) : ZoneRules

Creates ZoneRules with a fixed GMT offset.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Time.TimeZone.ZoneRules.UTC : ZoneRules

Creates ZoneRules with a fixed offset of UTC (GMT+0).

Equations

• Std.Time.TimeZone.ZoneRules.UTC = Std.Time.TimeZone.ZoneRules.fixedOffsetZone 0 (some "UTC") (some "UTC")

@[inline]

def Std.Time.TimeZone.ZoneRules.findLocalTimeTypeForTimestamp (zr : ZoneRules) (timestamp : Timestamp) : LocalTimeType

Finds the LocalTimeType corresponding to a given Timestamp in ZoneRules. If the timestamp falls between two transitions, it returns the most recent transition before the timestamp. If no transition is found, it falls back to initialLocalTimeType.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.TimeZone.ZoneRules.findLocalTimeTypeForWallTime (zr : ZoneRules) (wallTime : WallTime) : LocalTimeType

Finds the LocalTimeType for a given wall-clock time (seconds since 1970-01-01T00:00:00 in local time). Unlike findLocalTimeTypeForTimestamp, this compares each transition's UTC time adjusted by the previous offset — necessary when converting local time to UTC.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Time.TimeZone.ZoneRules.timezoneAt (zr : ZoneRules) (tm : Timestamp) : TimeZone

Find the current TimeZone out of a Transition in a ZoneRules

Equations

• zr.timezoneAt tm = (Std.Time.TimeZone.Transition.timezoneAt zr.transitions tm).toOption.getD zr.initialLocalTimeType.getTimeZone

@[inline]

def Std.Time.TimeZone.ZoneRules.ofTimeZone (tz : TimeZone) : ZoneRules

Creates ZoneRules for the given TimeZone.

Equations

• One or more equations did not get rendered due to their size.