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.

@[instance_reducible]

instance Std.Time.TimeZone.instReprUTLocal : Repr UTLocal

Equations

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

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

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

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

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

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

@[instance_reducible]

instance Std.Time.TimeZone.instReprTransition : Repr Transition

Equations

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

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

• transitionRule : Option RecurringRule

  Recurring rule from the TZif footer, used to extrapolate transitions beyond the last stored entry.

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

@[instance_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.findTransitionIndexForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Nat

Finds the index of the transition in effect at a given timestamp in Array Transition. Returns the index of the most recent transition that started at or before the timestamp, or none if the timestamp precedes all transitions.

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 in effect at a given timestamp in Array Transition. Returns the most recent transition that started at or before the timestamp, or none if the timestamp precedes all transitions.

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.RecurringRule.timezoneAt (rule : RecurringRule) (tm : Timestamp) : TimeZone

Returns the TimeZone in effect for this RecurringRule at the given Timestamp.

If no DST rule is defined, or if either transition rule is missing, the standard zone is returned unconditionally. Otherwise the function computes the UTC timestamps at which DST starts and ends for the year containing tm, and returns the DST zone when the timestamp falls inside the DST interval (accounting for rules that wrap across a year boundary in the Southern Hemisphere).

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

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. When the timestamp is beyond all stored transitions and a POSIX TZ footer rule is present, the rule is consulted. Falls back to initialLocalTimeType if no transition or rule applies.

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.

When the wall time falls beyond all stored transitions and a transitionRule is present, the recurring rule is used to determine the timezone (converting the wall time to UTC via the last known offset before consulting the rule).

Equations

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

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 = (zr.findLocalTimeTypeForTimestamp tm).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.