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

Equations

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

@[instance_reducible]

instance Std.Time.instReprFormatPart : Repr FormatPart

Equations

• Std.Time.instReprFormatPart = { reprPrec := Std.Time.instReprFormatPart.repr }

@[instance_reducible]

instance Std.Time.instCoeStringFormatPart : Coe String FormatPart

Equations

• Std.Time.instCoeStringFormatPart = { coe := Std.Time.FormatPart.string }

@[instance_reducible]

instance Std.Time.instCoeModifierFormatPart : Coe Modifier FormatPart

Equations

• Std.Time.instCoeModifierFormatPart = { coe := Std.Time.FormatPart.modifier }

@[reducible, inline]

abbrev Std.Time.FormatString : Type

The format of date and time string.

Equations

• Std.Time.FormatString = List Std.Time.FormatPart

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

Equations

• Std.Time.Awareness.instCoeTimeZone = { coe := Std.Time.Awareness.only }

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

Equations

• Std.Time.instInhabitedFormatConfig = { default := Std.Time.instInhabitedFormatConfig.default }

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

Equations

• Std.Time.instInhabitedGenericFormat = { default := Std.Time.instInhabitedGenericFormat.default }

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.

Equations

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

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

Equations

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

def Std.Time.TypeFormat : Modifier → Type

Equations

• Std.Time.TypeFormat (Std.Time.Modifier.G presentation) = Std.Time.Year.Era
• Std.Time.TypeFormat (Std.Time.Modifier.y presentation) = Std.Time.Year.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.u presentation) = Std.Time.Year.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.Y presentation) = Std.Time.Year.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.D presentation) = Sigma Std.Time.Day.Ordinal.OfYear
• Std.Time.TypeFormat (Std.Time.Modifier.M presentation) = Std.Time.Month.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.L presentation) = Std.Time.Month.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.d presentation) = Std.Time.Day.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.Q presentation) = Std.Time.Month.Quarter
• Std.Time.TypeFormat (Std.Time.Modifier.q presentation) = Std.Time.Month.Quarter
• Std.Time.TypeFormat (Std.Time.Modifier.w presentation) = Std.Time.Week.OfYear.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.W presentation) = Std.Time.Week.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.E presentation) = Std.Time.Weekday
• Std.Time.TypeFormat (Std.Time.Modifier.e presentation) = Std.Time.Weekday
• Std.Time.TypeFormat (Std.Time.Modifier.c presentation) = Std.Time.Weekday
• Std.Time.TypeFormat (Std.Time.Modifier.F presentation) = Std.Time.Week.Aligned.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.a presentation) = Std.Time.HourMarker
• Std.Time.TypeFormat (Std.Time.Modifier.b presentation) = Std.Time.DayPeriod
• Std.Time.TypeFormat (Std.Time.Modifier.B presentation) = Std.Time.ExtendedDayPeriod
• Std.Time.TypeFormat (Std.Time.Modifier.h presentation) = Std.Time.Internal.Bounded.LE 1 12
• Std.Time.TypeFormat (Std.Time.Modifier.K presentation) = Std.Time.Internal.Bounded.LE 0 11
• Std.Time.TypeFormat (Std.Time.Modifier.k presentation) = Std.Time.Internal.Bounded.LE 1 24
• Std.Time.TypeFormat (Std.Time.Modifier.H presentation) = Std.Time.Hour.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.m presentation) = Std.Time.Minute.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.s presentation) = Std.Time.Second.Ordinal true
• Std.Time.TypeFormat (Std.Time.Modifier.S presentation) = Std.Time.Nanosecond.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.A presentation) = Std.Time.Millisecond.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.n presentation) = Std.Time.Nanosecond.Ordinal
• Std.Time.TypeFormat (Std.Time.Modifier.N presentation) = Std.Time.Nanosecond.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.V presentation) = String
• Std.Time.TypeFormat (Std.Time.Modifier.z presentation) = String
• Std.Time.TypeFormat (Std.Time.Modifier.v presentation) = String
• Std.Time.TypeFormat (Std.Time.Modifier.O presentation) = Std.Time.TimeZone.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.X presentation) = Std.Time.TimeZone.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.x presentation) = Std.Time.TimeZone.Offset
• Std.Time.TypeFormat (Std.Time.Modifier.Z presentation) = Std.Time.TimeZone.Offset

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.

Equations

• Std.Time.parseMonthShort symbols = Std.Time.parseFromSymbols✝ (Std.Time.monthPairs✝ symbols.monthShort)

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

Equations

• Std.Time.FormatType result (Std.Time.FormatPart.modifier entry :: xs) = (Std.Time.TypeFormat entry → Std.Time.FormatType result xs)
• Std.Time.FormatType result (Std.Time.FormatPart.string val :: xs) = Std.Time.FormatType result xs
• Std.Time.FormatType result [] = result

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

Equations

• Std.Time.GenericFormat.spec input config = do let string ← Std.Time.specParser✝.run input pure { config := config, string := string }

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

Equations

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

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

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

Equations

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

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.

Equations

• Std.Time.GenericFormat.builderParser format config func = Std.Time.GenericFormat.builderParser.go✝ config format func

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

Parses the input string into a DateTime.

Equations

• format.parse input = (Std.Time.GenericFormat.parser✝ format.string format.config aw <* Std.Internal.Parsec.eof).run input

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.

Equations

• format.parse! input = match format.parse input with | Except.ok res => res | Except.error err => panicWithPosWithDecl "Std.Time.Format.Basic" "Std.Time.GenericFormat.parse!" 1124 18 err

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.

Equations

• format.parseBuilder builder input = (Std.Time.GenericFormat.builderParser format.string format.config builder).run input

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.

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.

Equations

• format.formatGeneric getInfo = Std.Time.GenericFormat.formatGeneric.go✝ getInfo format.config.dateformat "" format.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.

Equations

• format.formatBuilder = Std.Time.GenericFormat.formatBuilder.go✝ format.config.dateformat "" format.string

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

Equations

• Std.Time.instFormatGenericFormatFormatTypeString = { format := Std.Time.GenericFormat.formatBuilder, parse := fun {α : Type} => Std.Time.GenericFormat.parseBuilder }