inductive Std.Time.TimeZone.UTLocal : Type

Represents the type of local time in relation to UTC.

• ut : Std.Time.TimeZone.UTLocal

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

• local : Std.Time.TimeZone.UTLocal

  Local time that is not necessarily UTC.

instance Std.Time.TimeZone.instReprUTLocal : Repr Std.Time.TimeZone.UTLocal

Equations

• Std.Time.TimeZone.instReprUTLocal = { reprPrec := Std.Time.TimeZone.reprUTLocal✝ }

instance Std.Time.TimeZone.instInhabitedUTLocal : Inhabited Std.Time.TimeZone.UTLocal

Equations

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

inductive Std.Time.TimeZone.StdWall : Type

Represents types of wall clocks or standard times.

• wall : Std.Time.TimeZone.StdWall

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

• standard : Std.Time.TimeZone.StdWall

  Standard time without adjustments for daylight saving.

instance Std.Time.TimeZone.instReprStdWall : Repr Std.Time.TimeZone.StdWall

Equations

• Std.Time.TimeZone.instReprStdWall = { reprPrec := Std.Time.TimeZone.reprStdWall✝ }

instance Std.Time.TimeZone.instInhabitedStdWall : Inhabited Std.Time.TimeZone.StdWall

Equations

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

structure Std.Time.TimeZone.LocalTimeType : Type

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

• gmtOffset : Std.Time.TimeZone.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 : Std.Time.TimeZone.StdWall

  Indicates if the time is wall clock or standard time.

• utLocal : Std.Time.TimeZone.UTLocal

  Distinguishes between universal time and local time.

• identifier : String

  ID of the timezone

instance Std.Time.TimeZone.instReprLocalTimeType : Repr Std.Time.TimeZone.LocalTimeType

Equations

• Std.Time.TimeZone.instReprLocalTimeType = { reprPrec := Std.Time.TimeZone.reprLocalTimeType✝ }

instance Std.Time.TimeZone.instInhabitedLocalTimeType : Inhabited Std.Time.TimeZone.LocalTimeType

Equations

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

def Std.Time.TimeZone.LocalTimeType.getTimeZone (time : Std.Time.TimeZone.LocalTimeType) : Std.Time.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 : Std.Time.Second.Offset

  The specific time of the transition event.

• localTimeType : Std.Time.TimeZone.LocalTimeType

  The local time type associated with this transition.

instance Std.Time.TimeZone.instReprTransition : Repr Std.Time.TimeZone.Transition

Equations

• Std.Time.TimeZone.instReprTransition = { reprPrec := Std.Time.TimeZone.reprTransition✝ }

instance Std.Time.TimeZone.instInhabitedTransition : Inhabited Std.Time.TimeZone.Transition

Equations

• Std.Time.TimeZone.instInhabitedTransition = { default := { time := default, localTimeType := default } }

structure Std.Time.TimeZone.ZoneRules : Type

Represents the rules for a time zone.

• initialLocalTimeType : Std.Time.TimeZone.LocalTimeType

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

• transitions : Array Std.Time.TimeZone.Transition

  The array of transitions for the time zone.

instance Std.Time.TimeZone.instReprZoneRules : Repr Std.Time.TimeZone.ZoneRules

Equations

• Std.Time.TimeZone.instReprZoneRules = { reprPrec := Std.Time.TimeZone.reprZoneRules✝ }

instance Std.Time.TimeZone.instInhabitedZoneRules : Inhabited Std.Time.TimeZone.ZoneRules

Equations

• Std.Time.TimeZone.instInhabitedZoneRules = { default := { initialLocalTimeType := default, transitions := default } }

def Std.Time.TimeZone.Transition.createTimeZoneFromTransition (transition : Std.Time.TimeZone.Transition) : Std.Time.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 : Std.Time.Timestamp) (transition : Std.Time.TimeZone.Transition) : Std.Time.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 Std.Time.TimeZone.Transition) (timestamp : Std.Time.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 Std.Time.TimeZone.Transition) (timestamp : Std.Time.Timestamp) : Option Std.Time.TimeZone.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 Std.Time.TimeZone.Transition) (tm : Std.Time.Timestamp) : Except String Std.Time.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 : Std.Time.Second.Offset) (identifier abbreviation : Option String := none) : Std.Time.TimeZone.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 : Std.Time.TimeZone.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 : Std.Time.TimeZone.ZoneRules) (timestamp : Std.Time.Timestamp) : Std.Time.TimeZone.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.

@[inline]

def Std.Time.TimeZone.ZoneRules.timezoneAt (zr : Std.Time.TimeZone.ZoneRules) (tm : Std.Time.Timestamp) : Std.Time.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 : Std.Time.TimeZone) : Std.Time.TimeZone.ZoneRules

Creates ZoneRules for the given TimeZone.

Equations

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