This module defines the Modifier type and its sub-types, representing format pattern letters.

inductive Std.Time.Text : Type

Text represents different text formatting styles.

• short : Text

  Short form (e.g., "Tue")

• full : Text

  Full form (e.g., "Tuesday")

• narrow : Text

  Narrow form (e.g., "T")

• twoLetterShort : Text

  Two-letter short form (e.g., "Tu"). Produced only by 6-letter weekday patterns (EEEEEE, eeeeee, cccccc).

@[instance_reducible]

instance Std.Time.instReprText : Repr Text

def Std.Time.instReprText.repr : Text → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedText : Inhabited Text

def Std.Time.Text.classify (num : Nat) : Option Text

classify classifies the number of pattern letters into a Text type.

structure Std.Time.Number : Type

Number represents different number formatting styles.

• padding : Nat

  Minimum number of digits; output is zero-padded on the left to reach this width. Determined by the count of pattern letters.

@[instance_reducible]

instance Std.Time.instReprNumber : Repr Number

def Std.Time.instReprNumber.repr : Number → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedNumber : Inhabited Number

def Std.Time.classifyNumberText : Nat → Option (Number ⊕ Text)

classifyNumberText classifies the number of pattern letters into either a Number or Text.

inductive Std.Time.Fraction : Type

Fraction represents the fraction of a second, which can either be full nanoseconds or a truncated form with fewer digits.

• nano : Fraction

  Nanosecond precision (up to 9 digits)

• truncated (digits : Nat) : Fraction

  Truncated to digits digits (truncated, not rounded)

@[instance_reducible]

instance Std.Time.instReprFraction : Repr Fraction

def Std.Time.instReprFraction.repr : Fraction → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedFraction : Inhabited Fraction

def Std.Time.Fraction.classify (nat : Nat) : Option Fraction

classify classifies the number of pattern letters into either a Fraction. It's used for nano.

inductive Std.Time.Year : Type

Year represents different year formatting styles based on the number of pattern letters.

• any : Year

  Any size (e.g., "19000000000000")

• twoDigit : Year

  Two-digit year format (e.g., "23" for 2023)

• fourDigit : Year

  Four-digit year format (e.g., "2023")

• extended (num : Nat) : Year

  Extended year format for more than 4 digits (e.g., "002023")

@[instance_reducible]

instance Std.Time.instReprYear : Repr Year

def Std.Time.instReprYear.repr : Year → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedYear : Inhabited Year

def Std.Time.Year.classify (num : Nat) : Option Year

classify classifies the number of pattern letters into a Year format.

inductive Std.Time.ZoneId : Type

ZoneId represents different time zone ID formats based on the number of pattern letters.

• unknown : ZoneId

  Unknown zone placeholder (1 letter, V): always formats as "unk".

• short : ZoneId

  IANA time zone ID (2 letters, VV, e.g., "America/Los_Angeles").

• full : ZoneId

  Reserved for a future generic location format (VVVV). Currently formatted identically to short.

def Std.Time.instReprZoneId.repr : ZoneId → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprZoneId : Repr ZoneId

@[instance_reducible]

instance Std.Time.instInhabitedZoneId : Inhabited ZoneId

def Std.Time.ZoneId.classify (num : Nat) : Option ZoneId

classify classifies the number of pattern letters into a ZoneId format.

• If 1 letter, it returns the unknown form.
• If 2 letters, it returns the short form.
• If 4 letters, it returns the full form.
• Otherwise, it returns none.

inductive Std.Time.ZoneName : Type

ZoneName represents different zone name formats based on the number of pattern letters and whether daylight saving time is considered.

• short : ZoneName

  Short form of zone name (e.g., "PST")

• full : ZoneName

  Full form of zone name (e.g., "Pacific Standard Time")

def Std.Time.instReprZoneName.repr : ZoneName → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprZoneName : Repr ZoneName

@[instance_reducible]

instance Std.Time.instInhabitedZoneName : Inhabited ZoneName

def Std.Time.ZoneName.classify (letter : Char) (num : Nat) : Option ZoneName

classify classifies the number of pattern letters and the letter type ('z' or 'v') into a ZoneName format.

• For 'z', if less than 4 letters, it returns the short form; if 4 letters, it returns the full form.
• For 'v', if 1 letter, it returns the short form; if 4 letters, it returns the full form.
• Otherwise, it returns none.

inductive Std.Time.OffsetX : Type

OffsetX represents different offset formats based on the number of pattern letters. The output will vary between the number of pattern letters, whether it's the hour, minute, second, and whether colons are used.

• hour : OffsetX

  Only the hour is output (e.g., "+01")

• hourMinute : OffsetX

  Hour and minute without colon (e.g., "+0130")

• hourMinuteColon : OffsetX

  Hour and minute with colon (e.g., "+01:30")

• hourMinuteSecond : OffsetX

  Hour, minute, and second without colon (e.g., "+013015")

• hourMinuteSecondColon : OffsetX

  Hour, minute, and second with colon (e.g., "+01:30:15")

@[instance_reducible]

instance Std.Time.instReprOffsetX : Repr OffsetX

def Std.Time.instReprOffsetX.repr : OffsetX → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedOffsetX : Inhabited OffsetX

def Std.Time.OffsetX.classify (num : Nat) : Option OffsetX

classify classifies the number of pattern letters into an OffsetX format.

inductive Std.Time.OffsetO : Type

OffsetO represents localized offset text formats based on the number of pattern letters.

• short : OffsetO

  Short form of the localized offset (e.g., "GMT+8")

• full : OffsetO

  Full form of the localized offset (e.g., "GMT+08:00")

def Std.Time.instReprOffsetO.repr : OffsetO → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprOffsetO : Repr OffsetO

@[instance_reducible]

instance Std.Time.instInhabitedOffsetO : Inhabited OffsetO

def Std.Time.OffsetO.classify (num : Nat) : Option OffsetO

classify classifies the number of pattern letters into an OffsetO format.

inductive Std.Time.OffsetZ : Type

OffsetZ represents different offset formats based on the number of pattern letters (capital 'Z').

• hourMinute : OffsetZ

  Hour and minute without colon, with optional seconds (e.g., "+0130", "+013015")

• full : OffsetZ

  Localized offset text in full form (e.g., "GMT+08:00")

• hourMinuteSecondColon : OffsetZ

  Hour and minute with colon, with optional seconds, and "Z" for zero offset (e.g., "+01:30", "+01:30:15", "Z")

def Std.Time.instReprOffsetZ.repr : OffsetZ → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprOffsetZ : Repr OffsetZ

@[instance_reducible]

instance Std.Time.instInhabitedOffsetZ : Inhabited OffsetZ

def Std.Time.OffsetZ.classify (num : Nat) : Option OffsetZ

classify classifies the number of pattern letters into an OffsetZ format.

inductive Std.Time.DayPeriod : Type

DayPeriod extends HourMarker with exact noon and midnight values, used by the b pattern.

• am : DayPeriod

  Ante meridiem (before noon)

• pm : DayPeriod

  Post meridiem (after noon)

• noon : DayPeriod

  Exactly noon (12:00:00)

• midnight : DayPeriod

  Exactly midnight (00:00:00)

def Std.Time.instReprDayPeriod.repr : DayPeriod → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprDayPeriod : Repr DayPeriod

@[instance_reducible]

instance Std.Time.instInhabitedDayPeriod : Inhabited DayPeriod

inductive Std.Time.ExtendedDayPeriod : Type

ExtendedDayPeriod is a more granular day-period classification used by the B pattern, subdividing the day into named English CLDR segments.

• midnight : ExtendedDayPeriod

  Exactly 00:00:00

• night : ExtendedDayPeriod

  21:00–06:00 (exclusive of midnight)

• morning : ExtendedDayPeriod

  06:00–12:00

• noon : ExtendedDayPeriod

  Exactly 12:00:00

• afternoon : ExtendedDayPeriod

  12:00–18:00

• evening : ExtendedDayPeriod

  18:00–21:00

@[instance_reducible]

instance Std.Time.instReprExtendedDayPeriod : Repr ExtendedDayPeriod

def Std.Time.instReprExtendedDayPeriod.repr : ExtendedDayPeriod → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instInhabitedExtendedDayPeriod : Inhabited ExtendedDayPeriod

inductive Std.Time.Modifier : Type

Modifier represents a single format pattern letter with its presentation style.

The table below lists every symbol, its presentation type, the TypeFormat value type produced when parsing or consumed when formatting, and representative output examples.

Symbol  Meaning                        Presentation      TypeFormat                Examples
──────────────────────────────────────────────────────────────────────────────────────────────────
G       era                            Text              Year.Era                  AD; Anno Domini; A
u       year (proleptic/astronomical)  Year              Year.Offset               2004; 04; -0001; -1
y       year-of-era                    Year              Year.Offset               2004; 04; 0002; 2
D       day-of-year                    Number            Σ Day.Ordinal.OfYear      189
M/L     month-of-year                  Number ⊕ Text     Month.Ordinal             7; 07; Jul; July; J
d       day-of-month                   Number            Day.Ordinal               10
──────────────────────────────────────────────────────────────────────────────────────────────────
Q/q     quarter-of-year                Number ⊕ Text     Month.Quarter             3; 03; Q3; 3rd quarter
Y       week-based-year                Year              Year.Offset               1996; 96
w       week-of-week-based-year        Number            Week.Ordinal              27
W       week-of-month                  Number            Week.Ordinal.OfMonth      4
E       day-of-week (text only)        Text              Weekday                   Tue; Tuesday; T
e/c     localized day-of-week          Number ⊕ Text     Weekday                   2; 02; Tue; Tuesday; T
F       day-of-week-in-month           Number            Bounded.LE 1 5            3
──────────────────────────────────────────────────────────────────────────────────────────────────
a       am-pm-of-day                   Text              HourMarker                AM; PM
b       day-period (noon/midnight)     Text              DayPeriod                 AM; noon; midnight
B       extended day period            Text              ExtendedDayPeriod         in the morning; at night
h       clock-hour-of-am-pm (1-12)    Number            Bounded.LE 1 12           12
K       hour-of-am-pm (0-11)          Number            Bounded.LE 0 11           0
k       clock-hour-of-day (1-24)      Number            Bounded.LE 1 24           24
──────────────────────────────────────────────────────────────────────────────────────────────────
H       hour-of-day (0-23)            Number            Hour.Ordinal              0
m       minute-of-hour                Number            Minute.Ordinal            30
s       second-of-minute              Number            Second.Ordinal true       55
S       fraction-of-second            Fraction          Nanosecond.Ordinal        978
A       milli-of-day                  Number            Millisecond.Offset        1234
n       nano-of-second                Number            Nanosecond.Ordinal        987654321
N       nano-of-day                   Number            Nanosecond.Offset         1234000000
──────────────────────────────────────────────────────────────────────────────────────────────────
V       time-zone ID                  ZoneId            String                    America/Los_Angeles; Z
z       time-zone name                ZoneName          String                    Pacific Standard Time; PST
v       generic zone name             ZoneName          String                    Pacific Time; PT
O       localized zone-offset         OffsetO           Offset                    GMT+8; GMT+08:00
X       zone-offset ('Z' for zero)    OffsetX           Offset                    Z; -08; -0830; -08:30
x       zone-offset                   OffsetX           Offset                    +0000; -08; -0830; -08:30
Z       zone-offset                   OffsetZ           Offset                    +0000; -0800; -08:00

• G (presentation : Text) : Modifier

  G: Era (e.g., AD, Anno Domini, A).

• u (presentation : Year) : Modifier

  u: Proleptic/astronomical year (e.g., 2004, 04, -0001, -1). Can be negative: year 0 exists and -0001 = 2 BC. Use y + G instead when you want the era-based (always-positive) representation.

• y (presentation : Year) : Modifier

  y: Year of era (e.g., 2004, 04, 0002, 2). Never negative: year 1 BC is formatted as 1 paired with a BC era designator. Use u instead when you need the proleptic/astronomical year (which can be negative).

• D (presentation : Number) : Modifier

  D: Day of year (e.g., 189).

• M (presentation : Number ⊕ Text) : Modifier

  M: Month of year as number or text (e.g., 7, 07, Jul, July, J).

• L (presentation : Number ⊕ Text) : Modifier

  L: Stand-alone month of year as number or text (e.g., 7, 07, Jul, July, J). Stand-alone means the month is used independently (e.g., a calendar header "July") rather than as part of a full date. In practice the output is the same as M; the distinction is meaningful only in locale-aware contexts.

• d (presentation : Number) : Modifier

  d: Day of month (e.g., 10).

• Q (presentation : Number ⊕ Text) : Modifier

  Q: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).

• q (presentation : Number ⊕ Text) : Modifier

  q: Stand-alone quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter). Stand-alone means the value is used independently (e.g., a calendar header) rather than as part of a full date phrase. In practice the output is the same as Q; the distinction is meaningful only in locale-aware contexts.

• Y (presentation : Year) : Modifier

  Y: ISO week-based year (e.g., 2004, 04, 0002, 2). This is the year that contains the ISO week (w), which can differ from the calendar year near year boundaries: e.g., Dec 31 may belong to week 1 of the following year.

• w (presentation : Number) : Modifier

  w: Week of week-based year (e.g., 27).

• W (presentation : Number) : Modifier

  W: Week of month (e.g., 4).

• E (presentation : Text) : Modifier

  E: Day of week as text (e.g., Tue, Tuesday, T).

• e (presentation : Number ⊕ Text) : Modifier

  e: Day of week as number or text (e.g., 1, 01, Mon, Monday, M). The numeric value uses Monday=1 through Sunday=7 (ISO 8601 convention). Text output is the same as E.

• c (presentation : Number ⊕ Text) : Modifier

  c: Stand-alone day of week as number or text (e.g., 2, Tue, Tuesday, T). Stand-alone means the day is used independently (e.g., a calendar column header) rather than as part of a full date. Unlike e, cc (count of 2) is not valid; the minimum is c (1 letter) or ccc (3 letters).

• F (presentation : Number) : Modifier

  F: Day-of-week-in-month / occurrence of the weekday within the month (e.g., 2nd Sunday -> 2).

• a (presentation : Text) : Modifier

  a: AM/PM of day (e.g., PM).

• b (presentation : Text) : Modifier

  b: Day period with noon/midnight distinction (e.g., AM, noon, midnight).

• B (presentation : Text) : Modifier

  B: Extended day period with named segments (e.g., "in the morning", "at night").

• h (presentation : Number) : Modifier

  h: Clock hour of AM/PM (1-12) (e.g., 12).

• K (presentation : Number) : Modifier

  K: Hour of AM/PM (0-11) (e.g., 0).

• k (presentation : Number) : Modifier

  k: Clock hour of day (1-24) (e.g., 24).

• H (presentation : Number) : Modifier

  H: Hour of day (0-23) (e.g., 0).

• m (presentation : Number) : Modifier

  m: Minute of hour (e.g., 30).

• s (presentation : Number) : Modifier

  s: Second of minute (e.g., 55).

• S (presentation : Fraction) : Modifier

  S: Fraction of second (e.g., 978).

• A (presentation : Number) : Modifier

  A: Millisecond of day (e.g., 1234).

• n (presentation : Number) : Modifier

  n: Nanosecond of second (e.g., 987654321).

• N (presentation : Number) : Modifier

  N: Nanosecond of day (e.g., 1234000000).

• V (presentation : ZoneId) : Modifier

  V: Time zone ID.

  • V (1 letter): outputs "unk" (unknown zone placeholder per Unicode CLDR).
  • VV (2 letters): outputs the IANA zone ID (e.g., "America/Los_Angeles"), or "Z" for UTC.
• z (presentation : ZoneName) : Modifier

  z: Time zone name (e.g., Pacific Standard Time, PST).

• v (presentation : ZoneName) : Modifier

  v: Generic time zone name, without DST distinction (e.g., Pacific Time, PT).

• O (presentation : OffsetO) : Modifier

  O: Localized zone offset using the GMT prefix (e.g., GMT+8, GMT+08:00).

• X (presentation : OffsetX) : Modifier

  X: Zone offset with 'Z' for zero (e.g., Z, -08, -0830, -08:30).

• x (presentation : OffsetX) : Modifier

  x: Zone offset without 'Z' (e.g., +0000, -08, -0830, -08:30).

• Z (presentation : OffsetZ) : Modifier

  Z: Zone offset.

  • Z, ZZ, ZZZ: output ±HHMMss (no colon); parse ±HHMM[ss]. Does not accept the literal Z character for UTC — use ZZZZZ or XXX for that.
  • ZZZZ: outputs/parses localized GMT form (e.g., GMT+08:00).
  • ZZZZZ: outputs ±HH:mm[:ss] and uses Z for UTC (e.g., Z, +01:30).

def Std.Time.instReprModifier.repr : Modifier → Nat → Std.Format

@[instance_reducible]

instance Std.Time.instReprModifier : Repr Modifier

@[instance_reducible]

instance Std.Time.instInhabitedModifier : Inhabited Modifier

def Std.Time.parseModifier : Internal.Parsec.String.Parser Modifier

Parses a single format Modifier from the input string.