class Std.Time.Database (α : Type) : Type

A timezone database from which we can read the ZoneRules of some area by it's id.

• getZoneRules : α → String → IO TimeZone.ZoneRules

  Retrieves the zone rules information (ZoneRules) for a given area at a specific point in time.

• getLocalZoneRules : α → IO TimeZone.ZoneRules

  Retrieves the local zone rules information (ZoneRules) at a given timestamp.

def Std.Time.TimeZone.convertWall : Bool → StdWall

Converts a Boolean value to a corresponding StdWall type.

Equations

• Std.Time.TimeZone.convertWall true = Std.Time.TimeZone.StdWall.standard
• Std.Time.TimeZone.convertWall false = Std.Time.TimeZone.StdWall.wall

def Std.Time.TimeZone.convertUt : Bool → UTLocal

Converts a Boolean value to a corresponding UTLocal type.

Equations

• Std.Time.TimeZone.convertUt true = Std.Time.TimeZone.UTLocal.ut
• Std.Time.TimeZone.convertUt false = Std.Time.TimeZone.UTLocal.local

def Std.Time.TimeZone.convertLocalTimeType (index : Nat) (tz : TZif.TZifV1) (identifier : String) : Option LocalTimeType

Converts a given time index into a LocalTimeType by using a time zone (tz) and its identifier.

Equations

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

def Std.Time.TimeZone.convertTransition (times : Array LocalTimeType) (index : Nat) (tz : TZif.TZifV1) : Option Transition

Converts a transition.

Equations

• Std.Time.TimeZone.convertTransition times index tz = pure { time := Std.Time.Second.Offset.ofInt tz.transitionTimes[index]!, localTimeType := times[tz.transitionIndices[index]!.toNat]! }

def Std.Time.TimeZone.convertTZifV1 (tz : TZif.TZifV1) (id : String) : Except String ZoneRules

Converts a TZif.TZifV1 structure to a ZoneRules structure.

Equations

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

def Std.Time.TimeZone.convertTZifV2 (tz : TZif.TZifV2) (id : String) : Except String ZoneRules

Converts a TZif.TZifV2 structure to a ZoneRules structure.

Equations

• Std.Time.TimeZone.convertTZifV2 tz id = Std.Time.TimeZone.convertTZifV1 tz.toTZifV1 id

def Std.Time.TimeZone.convertTZif (tz : TZif.TZif) (id : String) : Except String ZoneRules

Converts a TZif.TZif structure to a ZoneRules structure.

Equations

• Std.Time.TimeZone.convertTZif tz id = match tz.v2 with | some v2 => Std.Time.TimeZone.convertTZifV2 v2 id | x => Std.Time.TimeZone.convertTZifV1 tz.v1 id