Parse and Format Specifier

The general form is %&lt;modifier>&lt;width><alternate>&lt;specifier>, where <modifier>, <width>, and <alternate> are optional.

modifier

glibc-style modifiers can be used before the specifier (here marked as z):

• %-z no padding

• %_z pad with spaces

• %0z pad with zeros

• %^z convert to upper case

• %#z convert to lower case (consistently, unlike glibc)

width

Width digits can also be used after any modifiers and before the specifier (here marked as z), for example:

• %4z pad to 4 characters (with default padding character)

• %_12z pad with spaces to 12 characters

alternate

An optional E character indicates an alternate formatting. Currently this only affects %Z and %z.

• %Ez alternate formatting

specifier

• %% %

• %t tab

• %n newline

• Specifier

• SubstituteSpecifier

inductive Time.Specifier : Type

• z : Specifier

  timezone offset in the format ±HHMM

• Ez : Specifier

  timezone offset in the format ±HH: MM

• Z : Specifier

  timezone name (or else offset in the format ±HHMM)

• EZ : Specifier

  timezone name (or else offset in the format ±HH: MM)

• P : Specifier

  day-half of day from (amPm locale), converted to lowercase, am, pm

• p : Specifier

  day-half of day from (amPm locale), AM, PM

• H : Specifier

  hour of day (24-hour), 0-padded to two chars, 00 - 23

• k : Specifier

  hour of day (24-hour), space-padded to two chars, 0 - 23

• I : Specifier

  hour of day-half (12-hour), 0-padded to two chars, 01 - 12

• l : Specifier

  hour of day-half (12-hour), space-padded to two chars, 1 - 12

• M : Specifier

  minute of hour, 0-padded to two chars, 00 - 59

• S : Specifier

  second of minute (without decimal part), 0-padded to two chars, 00 - 60

• q : Specifier

  picosecond of second, 0-padded to twelve chars, 000000000000 - 999999999999.

• Q : Specifier

  decimal point and fraction of second, up to 12 second decimals, without trailing zeros. For a whole number of seconds, %Q omits the decimal point unless padding is specified.

• u : Specifier

  day of week number for Week Date format, 1 (= Monday) - 7 (= Sunday)

• w : Specifier

  day of week number, 0 (= Sunday) - 6 (= Saturday)

• a : Specifier

  day of week, short form (snd from Time.TimeLocale.wDays locale), Sun - Sat

• A : Specifier

  day of week, long form (fst from Time.TimeLocale.wDays locale), Sunday - Saturday

• Y : Specifier

  year, no padding. Note %0Y and %_Y pad to four chars

• G : Specifier

  year, no padding. Note %0Y and %_Y pad to four chars

• y : Specifier

  year of century, 0-padded to two chars, 00 - 99

• g : Specifier

  year of century, 0-padded to two chars, 00 - 99

• C : Specifier

  century, no padding. Note %0C and %_C pad to two chars

• B : Specifier

  month name, long form (fst from Time.TimeLocale.months locale), January - December

• b : Specifier

  month name, short form (snd from Time.TimeLocale.months locale), Jan - Dec

• m : Specifier

  month of year, 0-padded to two chars, 01 - 12

• d : Specifier

  day of month, 0-padded to two chars, 01 - 31

• e : Specifier

  day of month, space-padded to two chars, 1 - 31

• j : Specifier

  day of year, 0-padded to three chars, 001 - 366

• f : Specifier

  century for Week Date format, no padding. Note %0f and %_f pad to two chars

• V : Specifier

  week of year for Week Date format, 0-padded to two chars, 01 - 53

• U : Specifier

  week of year where weeks start on Sunday (as sundayStartWeek), 0-padded to two chars, 00 - 53

• W : Specifier

  week of year where weeks start on Monday (as mondayStartWeek), 0-padded to two chars, 00 - 53

instance Time.instReprSpecifier : Repr Specifier

Equations

• Time.instReprSpecifier = { reprPrec := Time.reprSpecifier✝ }

instance Time.instBEqSpecifier : BEq Specifier

Equations

• Time.instBEqSpecifier = { beq := Time.beqSpecifier✝ }

inductive Time.SubstituteSpecifier : Type

• c : SubstituteSpecifier

  as 'dateTimeFmt' of Time.TimeLocale

• R : SubstituteSpecifier

  same as %H:%M

• T : SubstituteSpecifier

  same as %H:%M:%S

• X : SubstituteSpecifier

  as timeFmt of Time.TimeLocale (e.g. %H:%M:%S)

• r : SubstituteSpecifier

  as time12Fmt of Time.TimeLocale (e.g. %I:%M:%S %p)

• D : SubstituteSpecifier

  same as %m\/%d\/%y

• F : SubstituteSpecifier

  same as %Y-%m-%d

• x : SubstituteSpecifier

  as dateFmt of Time.TimeLocale (e.g. %m\/%d\/%y)

• h : SubstituteSpecifier

  month name, short form

def Time.toSpecifier : Char → Option Specifier

def Time.toSubstituteSpecifier : Char → Option SubstituteSpecifier

Equations

• Time.toSubstituteSpecifier 'c' = some Time.SubstituteSpecifier.c
• Time.toSubstituteSpecifier 'R' = some Time.SubstituteSpecifier.R
• Time.toSubstituteSpecifier 'T' = some Time.SubstituteSpecifier.T
• Time.toSubstituteSpecifier 'X' = some Time.SubstituteSpecifier.X
• Time.toSubstituteSpecifier 'r' = some Time.SubstituteSpecifier.r
• Time.toSubstituteSpecifier 'D' = some Time.SubstituteSpecifier.D
• Time.toSubstituteSpecifier 'F' = some Time.SubstituteSpecifier.F
• Time.toSubstituteSpecifier 'x' = some Time.SubstituteSpecifier.x
• Time.toSubstituteSpecifier 'h' = some Time.SubstituteSpecifier.h
• Time.toSubstituteSpecifier x✝ = none