This module defines the Formatter types. It is based on the Java's DateTimeFormatter format.

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")

@[implicit_reducible]

instance Std.Time.instReprText : Repr Text

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

@[implicit_reducible]

instance Std.Time.instInhabitedText : Inhabited Text

def Std.Time.instInhabitedText.default : 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

  The number of digits to pad, based on the count of pattern letters.

@[implicit_reducible]

instance Std.Time.instReprNumber : Repr Number

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

@[implicit_reducible]

instance Std.Time.instInhabitedNumber : Inhabited Number

def Std.Time.instInhabitedNumber.default : 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

  Fewer digits (truncated precision)

@[implicit_reducible]

instance Std.Time.instReprFraction : Repr Fraction

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

def Std.Time.instInhabitedFraction.default : Fraction

@[implicit_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")

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

@[implicit_reducible]

instance Std.Time.instReprYear : Repr Year

def Std.Time.instInhabitedYear.default : Year

@[implicit_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.

• short : ZoneId

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

• full : ZoneId

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

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

@[implicit_reducible]

instance Std.Time.instReprZoneId : Repr ZoneId

@[implicit_reducible]

instance Std.Time.instInhabitedZoneId : Inhabited ZoneId

def Std.Time.instInhabitedZoneId.default : ZoneId

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

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

• 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

@[implicit_reducible]

instance Std.Time.instReprZoneName : Repr ZoneName

@[implicit_reducible]

instance Std.Time.instInhabitedZoneName : Inhabited ZoneName

def Std.Time.instInhabitedZoneName.default : 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")

@[implicit_reducible]

instance Std.Time.instReprOffsetX : Repr OffsetX

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

def Std.Time.instInhabitedOffsetX.default : OffsetX

@[implicit_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")

@[implicit_reducible]

instance Std.Time.instReprOffsetO : Repr OffsetO

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

@[implicit_reducible]

instance Std.Time.instInhabitedOffsetO : Inhabited OffsetO

def Std.Time.instInhabitedOffsetO.default : 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 (e.g., "+0130")

• full : OffsetZ

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

• hourMinuteSecondColon : OffsetZ

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

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

@[implicit_reducible]

instance Std.Time.instReprOffsetZ : Repr OffsetZ

def Std.Time.instInhabitedOffsetZ.default : OffsetZ

@[implicit_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.Modifier : Type

The Modifier inductive type represents various formatting options for date and time components, matching the format symbols used in date and time strings. These modifiers can be applied in formatting functions to generate custom date and time outputs.

• G (presentation : Text) : Modifier

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

• y (presentation : Year) : Modifier

  y: Year of era (e.g., 2004, 04, 0002, 2).

• u (presentation : Year) : Modifier

  u: Year (e.g., 2004, 04, -0001, -1).

• D (presentation : Number) : Modifier

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

• MorL (presentation : Number ⊕ Text) : Modifier

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

• d (presentation : Number) : Modifier

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

• Qorq (presentation : Number ⊕ Text) : Modifier

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

• 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).

• eorc (presentation : Number ⊕ Text) : Modifier

  e: Localized day of week as number or text (e.g., 2, 02, Tue, Tuesday, T).

• F (presentation : Number) : Modifier

  F: Aligned week of month (e.g., 3).

• a (presentation : Text) : Modifier

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

• 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 : Modifier

  V: Time zone ID (e.g., America/Los_Angeles, Z, -08:30).

• z (presentation : ZoneName) : Modifier

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

• O (presentation : OffsetO) : Modifier

  O: Localized zone offset (e.g., GMT+8, GMT+08:00, UTC-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 with 'Z' for UTC (e.g., +0000, -0800, -08:00).

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

@[implicit_reducible]

instance Std.Time.instReprModifier : Repr Modifier

@[implicit_reducible]

instance Std.Time.instInhabitedModifier : Inhabited Modifier

def Std.Time.instInhabitedModifier.default : Modifier

inductive Std.Time.FormatPart : Type

The part of a formatting string. A string is just a text and a modifier is in the format described in the Modifier type.

• string (val : String) : FormatPart

  A string literal.

• modifier (modifier : Modifier) : FormatPart

  A modifier that renders some data into text.

def Std.Time.instReprFormatPart.repr : FormatPart → Nat → Std.Format

@[implicit_reducible]

instance Std.Time.instReprFormatPart : Repr FormatPart

@[implicit_reducible]

instance Std.Time.instCoeStringFormatPart : Coe String FormatPart

@[implicit_reducible]

instance Std.Time.instCoeModifierFormatPart : Coe Modifier FormatPart

@[reducible, inline]

abbrev Std.Time.FormatString : Type

The format of date and time string.

inductive Std.Time.Awareness : Type

If the format is aware of some timezone data it parses or if it parses any timezone.

• only : TimeZone → Awareness

  The format only parses a single timezone.

• any : Awareness

  The format parses any timezone.

@[implicit_reducible]

instance Std.Time.Awareness.instCoeTimeZone : Coe TimeZone Awareness

def Std.Time.Awareness.type (x : Awareness) : Type

structure Std.Time.FormatConfig : Type

Configuration options for formatting and parsing date/time strings.

• allowLeapSeconds : Bool

  Whether to allow leap seconds, such as 2016-12-31T23:59:60Z. Default is false.

@[implicit_reducible]

instance Std.Time.instInhabitedFormatConfig : Inhabited FormatConfig

def Std.Time.instInhabitedFormatConfig.default : FormatConfig

@[implicit_reducible]

instance Std.Time.instReprFormatConfig : Repr FormatConfig

def Std.Time.instReprFormatConfig.repr : FormatConfig → Nat → Std.Format

structure Std.Time.GenericFormat (awareness : Awareness) : Type

A specification on how to format a data or parse some string.

• config : FormatConfig

  Configuration options for formatting behavior.

• string : FormatString

  The format string used for parsing and formatting.

@[implicit_reducible]

instance Std.Time.instInhabitedGenericFormat {a✝ : Awareness} : Inhabited (GenericFormat a✝)

def Std.Time.instInhabitedGenericFormat.default {a✝ : Awareness} : GenericFormat a✝

def Std.Time.instReprGenericFormat.repr {awareness✝ : Awareness} : GenericFormat awareness✝ → Nat → Std.Format

@[implicit_reducible]

instance Std.Time.instReprGenericFormat {awareness✝ : Awareness} : Repr (GenericFormat awareness✝)

def Std.Time.TypeFormat : Modifier → Type

def Std.Time.parseMonthShort : Internal.Parsec.String.Parser Month.Ordinal

Parses a short value of a Month.Ordinal

def Std.Time.FormatType (result : Type) : FormatString → Type

def Std.Time.GenericFormat.spec {tz : Awareness} (input : String) (config : FormatConfig := { }) : Except String (GenericFormat tz)

Constructs a new GenericFormat specification for a date-time string. Modifiers can be combined to create custom formats, such as "YYYY, MMMM, D".

def Std.Time.GenericFormat.spec! {tz : Awareness} (input : String) (config : FormatConfig := { }) : GenericFormat tz

Builds a GenericFormat from the input string. If parsing fails, it will panic

def Std.Time.GenericFormat.format {aw : Awareness} {tz : TimeZone} (format : GenericFormat aw) (date : DateTime tz) : String

Formats a DateTime value into a string using the given GenericFormat.

def Std.Time.GenericFormat.builderParser {α : Type} (format : FormatString) (config : FormatConfig) (func : FormatType (Option α) format) : Internal.Parsec.String.Parser α

Parser for a format with a builder.

def Std.Time.GenericFormat.parse {aw : Awareness} (format : GenericFormat aw) (input : String) : Except String aw.type

Parses the input string into a ZoneDateTime.

def Std.Time.GenericFormat.parse! {aw : Awareness} (format : GenericFormat aw) (input : String) : aw.type

Parses the input string into a ZoneDateTime and panics if its wrong.

def Std.Time.GenericFormat.parseBuilder {aw : Awareness} {α : Type} (format : GenericFormat aw) (builder : FormatType (Option α) format.string) (input : String) : Except String α

Parses an input string using a builder function to produce a value.

def Std.Time.GenericFormat.parseBuilder! {α : Type} {aw : Awareness} [Inhabited α] (format : GenericFormat aw) (builder : FormatType (Option α) format.string) (input : String) : α

Parses an input string using a builder function, panicking on errors.

def Std.Time.GenericFormat.formatGeneric {aw : Awareness} (format : GenericFormat aw) (getInfo : (typ : Modifier) → Option (TypeFormat typ)) : Option String

Formats the date using the format into a String, using a getInfo function to get the information needed to build the String.

def Std.Time.GenericFormat.formatBuilder {aw : Awareness} (format : GenericFormat aw) : FormatType String format.string

Constructs a FormatType function to format a date into a string using a GenericFormat.

class Std.Time.Format (f : Type) (typ : Type → f → Type) : Type 1

Typeclass for formatting and parsing values with the given format type.

• format (fmt : f) : typ String fmt

  Converts a format f into a string.

• parse {α : Type} (fmt : f) : typ (Option α) fmt → String → Except String α

  Parses a string into a format using the provided format type f.

@[implicit_reducible]

instance Std.Time.instFormatGenericFormatFormatTypeString {aw : Awareness} : Format (GenericFormat aw) fun (x1 : Type) (x2 : GenericFormat aw) => FormatType x1 x2.string