source
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.

Instances

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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]! }

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For