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

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

@[instance_reducible]

instance Std.Time.instReprFormatPart : Repr FormatPart

@[instance_reducible]

instance Std.Time.instCoeStringFormatPart : Coe String FormatPart

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

@[instance_reducible]

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

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.

• dateformat : DateFormat

  Locale configuration for formatting and parsing, including locale-specific symbols and the first day of the week used for week-of-year and week-of-month calculations. Default is DateFormat.enUS (English, US).

@[instance_reducible]

instance Std.Time.instInhabitedFormatConfig : Inhabited FormatConfig

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.

@[instance_reducible]

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

def Std.Time.classifyDayPeriod (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : DayPeriod

Classify a PlainTime into a DayPeriod for the b pattern.

def Std.Time.classifyExtendedDayPeriod (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : ExtendedDayPeriod

Classify a PlainTime into an ExtendedDayPeriod for the B pattern (CLDR flexible periods).

def Std.Time.TypeFormat : Modifier → Type

def Std.Time.parseMonthShort (symbols : DateFormatSymbols) : Internal.Parsec.String.Parser Month.Ordinal

Parses a short month name using the given locale symbols and returns the corresponding 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} (format : GenericFormat aw) (date : DateTime) : 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 DateTime

Parses the input string into a DateTime.

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

Parses the input string into a DateTime 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.

@[instance_reducible]

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