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

Formats a PlainDate using a specific format.

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.

@[implicit_reducible]

instance Std.Time.PlainDate.instToString : ToString PlainDate

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

@[implicit_reducible]

instance Std.Time.PlainTime.instToString : ToString PlainTime

@[implicit_reducible]

instance Std.Time.PlainTime.instRepr : Repr PlainTime

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

Formats a ZonedDateTime using a specific format.

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

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

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

Formats a ZonedDateTime value into an ISO8601 string.

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

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

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

Formats a ZonedDateTime value into an RFC822 format string.

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

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

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

Formats a ZonedDateTime value into an RFC850 format string.

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

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

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

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

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

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

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

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

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

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

def Std.Time.ZonedDateTime.toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : 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.ZonedDateTime.parse (input : String) : Except String ZonedDateTime

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

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instToString : ToString ZonedDateTime

@[implicit_reducible]

instance Std.Time.ZonedDateTime.instRepr : Repr ZonedDateTime

def Std.Time.PlainDateTime.format (date : PlainDateTime) (format : String) : String

Formats a PlainDateTime using a specific format.

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 in the DateTime format and returns a PlainDateTime.

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

Formats a PlainDateTime value into a DateTime format string.

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

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

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

Formats a PlainDateTime value into a DateTime 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.

@[implicit_reducible]

instance Std.Time.PlainDateTime.instToString : ToString PlainDateTime

@[implicit_reducible]

instance Std.Time.PlainDateTime.instRepr : Repr PlainDateTime

def Std.Time.DateTime.format {tz : TimeZone} (data : DateTime tz) (format : String) : String

Formats a DateTime using a specific format.

def Std.Time.DateTime.fromAscTimeString (input : String) : Except String (DateTime TimeZone.GMT)

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

def Std.Time.DateTime.toAscTimeString (datetime : DateTime TimeZone.GMT) : String

Formats a DateTime value into an AscTime format string.

def Std.Time.DateTime.fromLongDateFormatString (input : String) : Except String (DateTime TimeZone.GMT)

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

def Std.Time.DateTime.toLongDateFormatString (datetime : DateTime TimeZone.GMT) : String

Formats a DateTime value into a LongDateFormat string.

def Std.Time.DateTime.toISO8601String {tz : TimeZone} (date : DateTime tz) : String

Formats a DateTime value into an ISO8601 string.

def Std.Time.DateTime.toRFC822String {tz : TimeZone} (date : DateTime tz) : String

Formats a DateTime value into an RFC822 format string.

def Std.Time.DateTime.toRFC850String {tz : TimeZone} (date : DateTime tz) : String

Formats a DateTime value into an RFC850 format string.

def Std.Time.DateTime.toDateTimeWithZoneString {tz : TimeZone} (pdt : DateTime tz) : String

Formats a DateTime value into a DateTimeWithZone format string.

def Std.Time.DateTime.toLeanDateTimeWithZoneString {tz : TimeZone} (pdt : DateTime tz) : String

Formats a DateTime value into a DateTimeWithZone format string that can be parsed by date%.

def Std.Time.DateTime.parse (date : String) : Except String (DateTime TimeZone.GMT)

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

@[implicit_reducible]

instance Std.Time.DateTime.instRepr {tz : TimeZone} : Repr (DateTime tz)

@[implicit_reducible]

instance Std.Time.DateTime.instToString {tz : TimeZone} : ToString (DateTime tz)