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

def Std.Time.TimeZone.instInhabitedUTLocal.default : 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

def Std.Time.TimeZone.instInhabitedStdWall.default : StdWall

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

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

@[implicit_reducible]

instance Std.Time.TimeZone.instReprLocalTimeType : Repr LocalTimeType

def Std.Time.TimeZone.instInhabitedLocalTimeType.default : LocalTimeType

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

def Std.Time.TimeZone.instInhabitedTransition.default : 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.

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

@[implicit_reducible]

instance Std.Time.TimeZone.instReprZoneRules : Repr ZoneRules

def Std.Time.TimeZone.instInhabitedZoneRules.default : ZoneRules

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedZoneRules : Inhabited ZoneRules

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.

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