Types for recurring DST transition rules, used by ZoneRules and produced by POSIX TZ parsing.

inductive Std.Time.TimeZone.TransitionSpec : Type

Specifies how a DST transition date is expressed.

• mwd (month : Month.Ordinal) (week : Week.Aligned.Ordinal) (day : Weekday.Ordinal) : TransitionSpec

  Mm.w.d form: month m, week w (1–5; 5 = last), ISO weekday d.

• julian (day : Internal.Bounded.LE 1 365) : TransitionSpec

  Jn form: Julian day 1–365 (Feb 29 never counted, even in leap years).

• julian0 (day : Internal.Bounded.LE 0 365) : TransitionSpec

  n form: zero-based day 0–365 (Feb 29 counted in leap years).

def Std.Time.TimeZone.instReprTransitionSpec.repr : TransitionSpec → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Std.Time.TimeZone.instReprTransitionSpec : Repr TransitionSpec

Equations

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

def Std.Time.TimeZone.TransitionSpec.toEpochDayMWD (year : Year.Offset) (month : Month.Ordinal) (week : Week.Aligned.Ordinal) (day : Weekday.Ordinal) : Day.Offset

Returns the Day.Offset (days since epoch) for a TransitionSpec.mwd in the given year.

Mm.w.d: month m, week w (1–5; 5 = last), ISO weekday d (1 = Monday, 7 = Sunday). Finds the w-th occurrence of weekday d in month m; if w = 5, returns the last occurrence.

Equations

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

def Std.Time.TimeZone.TransitionSpec.toEpochDayJulian (year : Year.Offset) (day : Internal.Bounded.LE 1 365) : Day.Offset

Returns the Day.Offset (days since epoch) for a TransitionSpec.julian in the given year.

Jn: Julian day 1–365. Feb 29 is never counted, so in a leap year days ≥ 60 are shifted by one.

Equations

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

def Std.Time.TimeZone.TransitionSpec.toEpochDayJulian0 (year : Year.Offset) (day : Internal.Bounded.LE 0 365) : Day.Offset

Returns the Day.Offset (days since epoch) for a TransitionSpec.julian0 in the given year.

n: zero-based day 0–365. Feb 29 is counted normally in leap years.

Equations

• Std.Time.TimeZone.TransitionSpec.toEpochDayJulian0 year day = (Std.Time.PlainDate.ofYearMonthDayClip year 1 1).toEpochDay + Std.Time.Day.Offset.ofInt day.val

def Std.Time.TimeZone.TransitionSpec.toEpochDay (spec : TransitionSpec) (year : Year.Offset) : Day.Offset

Returns the Day.Offset (days since epoch) for this TransitionSpec in the given year.

Equations

• (Std.Time.TimeZone.TransitionSpec.mwd a a_1 a_2).toEpochDay year = Std.Time.TimeZone.TransitionSpec.toEpochDayMWD year a a_1 a_2
• (Std.Time.TimeZone.TransitionSpec.julian a).toEpochDay year = Std.Time.TimeZone.TransitionSpec.toEpochDayJulian year a
• (Std.Time.TimeZone.TransitionSpec.julian0 a).toEpochDay year = Std.Time.TimeZone.TransitionSpec.toEpochDayJulian0 year a

structure Std.Time.TimeZone.TransitionRule : Type

A single DST transition rule: a date specification and a wall-clock time.

• spec : TransitionSpec

  How the transition date is specified.

• time : Second.Offset

  Time of day as seconds from midnight (default 7200 = 02:00).

  "The time has the same format as offset except that no leading sign ( '-' or '+' ) is allowed. The default, if time is not given, shall be 02:00:00." $8.3 https://pubs.opengroup.org/onlinepubs/9699919799/

@[instance_reducible]

instance Std.Time.TimeZone.instReprTransitionRule : Repr TransitionRule

Equations

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

def Std.Time.TimeZone.instReprTransitionRule.repr : TransitionRule → Nat → Std.Format

Equations

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

structure Std.Time.TimeZone.DaylightSavingRule : Type

Recurring DST details for a zone that observes daylight saving time.

• name : String

  DST abbreviation.

• offset : Offset

  DST UTC offset (east-positive).

• start : Option TransitionRule

  Rule for the start of DST, if any.

• end_ : Option TransitionRule

  Rule for the end of DST, if any.

@[instance_reducible]

instance Std.Time.TimeZone.instReprDaylightSavingRule : Repr DaylightSavingRule

Equations

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

def Std.Time.TimeZone.instReprDaylightSavingRule.repr : DaylightSavingRule → Nat → Std.Format

Equations

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

structure Std.Time.TimeZone.RecurringRule : Type

Recurring rule describing standard and DST zones, as found in a POSIX TZ string or TZif footer.

• stdName : String

  Standard time abbreviation.

• stdOffset : Offset

  Standard UTC offset (east-positive).

• dst : Option DaylightSavingRule

  DST details, if this zone observes DST.

def Std.Time.TimeZone.instReprRecurringRule.repr : RecurringRule → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Std.Time.TimeZone.instReprRecurringRule : Repr RecurringRule

Equations

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