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

          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

                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

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

                      Equations
                        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
                                    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

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

                                        Equations
                                          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

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

                                              Equations
                                                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

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

                                                    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

                                                          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
                                                            @[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
                                                                    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
                                                                      instance Std.Time.instReprGenericFormat {awareness✝ : Awareness} :
                                                                      Repr (GenericFormat awareness✝)
                                                                      Equations

                                                                        Parses a short value of a Month.Ordinal

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

                                                                                        Parser for a format with a builder.

                                                                                        Equations
                                                                                          Instances For

                                                                                            Parses the input string into a ZoneDateTime.

                                                                                            Equations
                                                                                              Instances For

                                                                                                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 : Std.Time.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 : Std.Time.FormatType✝ (Option α) format.string) (input : String) :
                                                                                                        α

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

                                                                                                        Equations
                                                                                                          Instances For

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