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

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

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
inductive Std.Time.Year :

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

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

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

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.

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

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

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

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

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

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

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

  • string : FormatString

    The format that is not aware of the timezone.

Instances For

Parses a short value of a Month.Ordinal

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

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

Equations

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

Parses the input string into a ZoneDateTime.

Equations

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

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

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

Equations
Equations

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

Equations
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