Documentation

Std.Time.Format.Basic

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

inductive Std.Time.Text :

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

Instances For

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

    Equations
    Instances For

      Number represents different number formatting styles.

      • padding : Nat

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

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

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

          Equations
          Instances For

            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)

            Instances For
              Equations
              Instances For

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

                Equations
                Instances For
                  inductive Std.Time.Year :

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

                  Instances For
                    Equations
                    Instances For

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

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

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

                        Instances For

                          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.
                          Equations
                          Instances For

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

                            Instances For

                              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.
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

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

                                Instances For
                                  Equations
                                  Instances For

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

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

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

                                      Instances For

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

                                        Instances For
                                          Equations
                                          Instances For

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

                                            Instances For
                                              Equations
                                              Instances For

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

                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[reducible, inline]

                                                    The format of date and time string.

                                                    Equations
                                                    Instances For

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

                                                      Instances For

                                                        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.

                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            structure Std.Time.GenericFormat (awareness : Awareness) :

                                                            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.

                                                            Instances For
                                                              def Std.Time.instReprGenericFormat.repr {awareness✝ : Awareness} :
                                                              GenericFormat awareness✝NatStd.Format
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                Instances For

                                                                  Parses a short value of a Month.Ordinal

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

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

                                                                    Equations
                                                                    Instances For

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

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        def Std.Time.GenericFormat.format {aw : Awareness} {tz : TimeZone} (format : GenericFormat aw) (date : DateTime tz) :

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

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

                                                                          Parser for a format with a builder.

                                                                          Equations
                                                                          Instances For

                                                                            Parses the input string into a ZoneDateTime.

                                                                            Equations
                                                                            Instances For
                                                                              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.

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

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

                                                                                Equations
                                                                                Instances For
                                                                                  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.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    def Std.Time.GenericFormat.formatGeneric {aw : Awareness} (format : GenericFormat aw) (getInfo : (typ : Modifier) → Option (TypeFormat typ)) :

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

                                                                                    Equations
                                                                                    Instances For

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

                                                                                      Equations
                                                                                      Instances For
                                                                                        class Std.Time.Format (f : Type) (typ : TypefType) :

                                                                                        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 α) fmtStringExcept String α

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

                                                                                        Instances