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: Time.Specifier

  timezone offset in the format ±HHMM

• Ez: Time.Specifier

  timezone offset in the format ±HH: MM

• Z: Time.Specifier

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

• EZ: Time.Specifier

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

• P: Time.Specifier

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

• p: Time.Specifier

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

• H: Time.Specifier

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

• k: Time.Specifier

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

• I: Time.Specifier

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

• l: Time.Specifier

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

• M: Time.Specifier

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

• S: Time.Specifier

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

• q: Time.Specifier

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

• Q: Time.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: Time.Specifier

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

• w: Time.Specifier

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

• a: Time.Specifier

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

• A: Time.Specifier

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

• Y: Time.Specifier

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

• G: Time.Specifier

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

• y: Time.Specifier

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

• g: Time.Specifier

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

• C: Time.Specifier

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

• B: Time.Specifier

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

• b: Time.Specifier

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

• m: Time.Specifier

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

• d: Time.Specifier

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

• e: Time.Specifier

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

• j: Time.Specifier

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

• f: Time.Specifier

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

• V: Time.Specifier

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

• U: Time.Specifier

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

• W: Time.Specifier

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

instance Time.instReprSpecifier : Repr Time.Specifier

Equations

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

instance Time.instBEqSpecifier : BEq Time.Specifier

Equations

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

inductive Time.SubstituteSpecifier : Type

• c: Time.SubstituteSpecifier

  as 'dateTimeFmt' of Time.TimeLocale

• R: Time.SubstituteSpecifier

  same as %H:%M

• T: Time.SubstituteSpecifier

  same as %H:%M:%S

• X: Time.SubstituteSpecifier

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

• r: Time.SubstituteSpecifier

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

• D: Time.SubstituteSpecifier

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

• F: Time.SubstituteSpecifier

  same as %Y-%m-%d

• x: Time.SubstituteSpecifier

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

• h: Time.SubstituteSpecifier

  month name, short form

def Time.toSpecifier : Char → Option Time.Specifier

Equations

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

def Time.toSubstituteSpecifier : Char → Option Time.SubstituteSpecifier

Equations

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