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

@[implicit_reducible]

instance Std.Time.TimeZone.instReprUTLocal : Repr UTLocal

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedUTLocal : Inhabited UTLocal

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

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

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedStdWall : Inhabited StdWall

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

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

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedLocalTimeType : Inhabited LocalTimeType

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

Gets the TimeZone offset from a LocalTimeType.

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

@[implicit_reducible]

instance Std.Time.TimeZone.instReprTransition : Repr Transition

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedTransition : Inhabited Transition

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

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

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedZoneRules : Inhabited ZoneRules

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

Returns the transition time as a Timestamp.

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

Create a TimeZone from a Transition.

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

Applies the transition to a Timestamp.

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.

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.

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

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

Creates ZoneRules with a fixed GMT offset.

@[inline]

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

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

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

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.

@[inline]

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

Find the current TimeZone out of a Transition in a ZoneRules

@[inline]

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

Creates ZoneRules for the given TimeZone.