def Std.Time.Formats.iso8601 : GenericFormat Awareness.any

The ISO 8601 format, used for representing date and time in a standardized format. The format follows the pattern uuuu-MM-dd'T'HH:mm:ssXXX.

def Std.Time.Formats.americanDate : GenericFormat Awareness.any

The americanDate format, which follows the pattern MM-dd-uuuu.

def Std.Time.Formats.europeanDate : GenericFormat Awareness.any

The europeanDate format, which follows the pattern dd-MM-uuuu.

def Std.Time.Formats.time12Hour : GenericFormat Awareness.any

The time12Hour format, which follows the pattern hh:mm:ss aa for representing time in a 12-hour clock format with an upper case AM/PM marker.

def Std.Time.Formats.time24Hour : GenericFormat Awareness.any

The Time24Hour format, which follows the pattern HH:mm:ss for representing time in a 24-hour clock format.

def Std.Time.Formats.dateTime24Hour : GenericFormat (Awareness.only TimeZone.GMT)

The DateTimeZone24Hour format, which follows the pattern uuuu-MM-dd:HH:mm:ss.SSSSSSSSS for representing date, time, and time zone.

def Std.Time.Formats.dateTimeWithZone : GenericFormat Awareness.any

The DateTimeWithZone format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ for representing date, time, and time zone.

def Std.Time.Formats.leanTime24Hour : GenericFormat Awareness.any

The leanTime24Hour format, which follows the pattern HH:mm:ss.SSSSSSSSS for representing time in a 24-hour clock format. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanTime24HourNoNanos : GenericFormat Awareness.any

The leanTime24HourNoNanos format, which follows the pattern HH:mm:ss for representing time in a 24-hour clock format. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTime24Hour : GenericFormat (Awareness.only TimeZone.GMT)

The leanDateTime24Hour format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTime24HourNoNanos : GenericFormat (Awareness.only TimeZone.GMT)

The leanDateTime24HourNoNanos format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTimeWithZone : GenericFormat Awareness.any

The leanDateTimeWithZone format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTimeWithZoneNoNanos : GenericFormat Awareness.any

The leanDateTimeWithZoneNoNanos format, which follows the pattern uuuu-MM-dd'T'HH:mm:ssZZZZZ for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTimeWithIdentifier : GenericFormat Awareness.any

The leanDateTimeWithIdentifier format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss[z] for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDateTimeWithIdentifierAndNanos : GenericFormat Awareness.any

The leanDateTimeWithIdentifierAndNanos format, which follows the pattern uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'[z]' for representing date, time, and time zone. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.leanDate : GenericFormat Awareness.any

The Lean Date format, which follows the pattern uuuu-MM-dd. It uses the default value that can be parsed with the notation of dates.

def Std.Time.Formats.sqlDate : GenericFormat Awareness.any

The SQLDate format, which follows the pattern uuuu-MM-dd and is commonly used in SQL databases to represent dates.

def Std.Time.Formats.longDateFormat : GenericFormat (Awareness.only TimeZone.GMT)

The LongDateFormat, which follows the pattern EEEE, MMMM d, uuuu HH:mm:ss for representing a full date and time with the day of the week and month name.

def Std.Time.Formats.ascTime : GenericFormat (Awareness.only TimeZone.GMT)

The AscTime format, which follows the pattern EEE MMM d HH:mm:ss uuuu. This format is often used in older systems for logging and time-stamping events.

def Std.Time.Formats.rfc822 : GenericFormat Awareness.any

The RFC822 format, which follows the pattern eee, dd MMM uuuu HH:mm:ss ZZZ. This format is used in email headers and HTTP headers.

def Std.Time.Formats.rfc850 : GenericFormat Awareness.any

The RFC850 format, which follows the pattern eee, dd-MMM-YY HH:mm:ss ZZZ. This format is an older standard for representing date and time in headers.

def Std.Time.Formats.httpDate : GenericFormat (Awareness.only TimeZone.GMT)

The HTTP-date format of RFC 9110 §5.6.7 (IMF-fixdate), which follows the pattern eee, dd MMM uuuu HH:mm:ss 'GMT', for example Sun, 06 Nov 1994 08:49:37 GMT. This is the format to use when generating HTTP header fields such as Date, Last-Modified and Expires. The zone is always the literal GMT; dates in other zones are converted when formatting.

def Std.Time.TimeZone.fromTimeZone (input : String) : Except String TimeZone

Parses a string into a TimeZone object. The input string must be in the format "VV ZZZZZ".

def Std.Time.TimeZone.Offset.fromOffset (input : String) : Except String Offset

Parses a string representing an offset into an Offset object. The input string must follow the "xxx" format.

def Std.Time.PlainDate.format (date : PlainDate) (format : String) (locale : DateFormat := DateFormat.enUS) : String

Formats a PlainDate using a specific format and locale.

def Std.Time.PlainDate.fromAmericanDateString (input : String) : Except String PlainDate

Parses a date string in the American format (MM-dd-uuuu) and returns a PlainDate.

def Std.Time.PlainDate.toAmericanDateString (input : PlainDate) : String

Converts a date in the American format (MM-dd-uuuu) into a String.

def Std.Time.PlainDate.fromSQLDateString (input : String) : Except String PlainDate

Parses a date string in the SQL format (uuuu-MM-dd) and returns a PlainDate.

def Std.Time.PlainDate.toSQLDateString (input : PlainDate) : String

Converts a date in the SQL format (uuuu-MM-dd) into a String.

def Std.Time.PlainDate.fromLeanDateString (input : String) : Except String PlainDate

Parses a date string in the Lean format (uuuu-MM-dd) and returns a PlainDate.

def Std.Time.PlainDate.toLeanDateString (input : PlainDate) : String

Converts a date in the Lean format (uuuu-MM-dd) into a String.

def Std.Time.PlainDate.parse (input : String) : Except String PlainDate

Parses a String in the AmericanDate or SQLDate format and returns a PlainDate.

@[instance_reducible]

instance Std.Time.PlainDate.instToString : ToString PlainDate

@[instance_reducible]

instance Std.Time.PlainDate.instRepr : Repr PlainDate

def Std.Time.PlainTime.format (time : PlainTime) (format : String) : String

Formats a PlainTime using a specific format.

def Std.Time.PlainTime.fromTime24Hour (input : String) : Except String PlainTime

Parses a time string in the 24-hour format (HH:mm:ss) and returns a PlainTime.

def Std.Time.PlainTime.toTime24Hour (input : PlainTime) : String

Formats a PlainTime value into a 24-hour format string (HH:mm:ss).

def Std.Time.PlainTime.fromLeanTime24Hour (input : String) : Except String PlainTime

Parses a time string in the lean 24-hour format (HH:mm:ss.SSSSSSSSS or HH:mm:ss) and returns a PlainTime.

def Std.Time.PlainTime.toLeanTime24Hour (input : PlainTime) : String

Formats a PlainTime value into a 24-hour format string (HH:mm:ss.SSSSSSSSS).

def Std.Time.PlainTime.fromTime12Hour (input : String) : Except String PlainTime

Parses a time string in the 12-hour format (hh:mm:ss aa) and returns a PlainTime.

def Std.Time.PlainTime.toTime12Hour (input : PlainTime) : String

Formats a PlainTime value into a 12-hour format string (hh:mm:ss aa).

def Std.Time.PlainTime.parse (input : String) : Except String PlainTime

Parses a String in the Time12Hour or Time24Hour format and returns a PlainTime.

@[instance_reducible]

instance Std.Time.PlainTime.instToString : ToString PlainTime

@[instance_reducible]

instance Std.Time.PlainTime.instRepr : Repr PlainTime

def Std.Time.DateTime.format (data : DateTime) (format : String) : String

Formats a DateTime using a specific format.

def Std.Time.DateTime.fromISO8601String (input : String) : Except String DateTime

Parses a String in the ISO8601 format and returns a DateTime.

def Std.Time.DateTime.toISO8601String (date : DateTime) : String

Formats a DateTime value into an ISO8601 string.

def Std.Time.DateTime.fromRFC822String (input : String) : Except String DateTime

Parses a String in the rfc822 format and returns a DateTime.

def Std.Time.DateTime.toRFC822String (date : DateTime) : String

Formats a DateTime value into an RFC822 format string.

def Std.Time.DateTime.fromRFC850String (input : String) : Except String DateTime

Parses a String in the rfc850 format and returns a DateTime.

def Std.Time.DateTime.toRFC850String (date : DateTime) : String

Formats a DateTime value into an RFC850 format string.

def Std.Time.DateTime.toHTTPDateString (date : DateTime) : String

Formats a DateTime as an HTTP-date (RFC 9110 §5.6.7), for example Sun, 06 Nov 1994 08:49:37 GMT. The result is always in GMT, whatever the zone of date.

def Std.Time.DateTime.fromHTTPDateString (input : String) : Except String DateTime

Parses an HTTP-date (RFC 9110 §5.6.7). Accepts the preferred form produced by toHTTPDateString and the two obsolete forms that recipients are required to accept: RFC 850 (Sunday, 06-Nov-94 08:49:37 GMT) and asctime (Sun Nov 6 08:49:37 1994). A two-digit RFC 850 year yy is read as 19yy when yy ≥ 70 and as 20yy otherwise.

def Std.Time.DateTime.fromDateTimeWithZoneString (input : String) : Except String DateTime

Parses a String in the dateTimeWithZone format and returns a DateTime object in the GMT time zone.

def Std.Time.DateTime.toDateTimeWithZoneString (pdt : DateTime) : String

Formats a DateTime value into a simple date time with timezone string.

def Std.Time.DateTime.fromLeanDateTimeWithZoneString (input : String) : Except String DateTime

Parses a String in the lean date time format with timezone format and returns a DateTime object.

def Std.Time.DateTime.fromLeanDateTimeWithIdentifierString (input : String) : Except String DateTime

Parses a String in the lean date time format with identifier and returns a DateTime object.

def Std.Time.DateTime.toLeanDateTimeWithZoneString (zdt : DateTime) : String

Formats a DateTime value into a simple date time with timezone string that can be parsed by the date% notation.

def Std.Time.DateTime.toLeanDateTimeWithIdentifierString (zdt : DateTime) : String

Formats a DateTime value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.

def Std.Time.DateTime.parse (input : String) : Except String DateTime

Parses a String in the ISO8601, RFC822 or RFC850 format and returns a DateTime.

@[instance_reducible]

instance Std.Time.DateTime.instToString : ToString DateTime

@[instance_reducible]

instance Std.Time.DateTime.instRepr : Repr DateTime

def Std.Time.PlainDateTime.format (date : PlainDateTime) (format : String) (locale : DateFormat := DateFormat.enUS) : String

Formats a PlainDateTime using a specific format and locale.

def Std.Time.PlainDateTime.fromAscTimeString (input : String) : Except String PlainDateTime

Parses a String in the AscTime format and returns a PlainDateTime object in the GMT time zone.

def Std.Time.PlainDateTime.toAscTimeString (pdt : PlainDateTime) : String

Formats a PlainDateTime value into an AscTime format string.

def Std.Time.PlainDateTime.fromLongDateFormatString (input : String) : Except String PlainDateTime

Parses a String in the LongDateFormat and returns a PlainDateTime object in the GMT time zone.

def Std.Time.PlainDateTime.toLongDateFormatString (pdt : PlainDateTime) : String

Formats a PlainDateTime value into a LongDateFormat string.

def Std.Time.PlainDateTime.fromDateTimeString (input : String) : Except String PlainDateTime

Parses a String and returns a PlainDateTime.

def Std.Time.PlainDateTime.toDateTimeString (pdt : PlainDateTime) : String

Formats a PlainDateTime value into a date time format string.

def Std.Time.PlainDateTime.fromLeanDateTimeString (input : String) : Except String PlainDateTime

Parses a String and returns a PlainDateTime.

def Std.Time.PlainDateTime.toLeanDateTimeString (pdt : PlainDateTime) : String

Formats a PlainDateTime value into a leanDateTime24Hour format string.

def Std.Time.PlainDateTime.parse (date : String) : Except String PlainDateTime

Parses a String in the AscTime or LongDate format and returns a PlainDateTime.

@[instance_reducible]

instance Std.Time.PlainDateTime.instToString : ToString PlainDateTime

@[instance_reducible]

instance Std.Time.PlainDateTime.instRepr : Repr PlainDateTime