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.

Equations

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

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

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

Equations

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

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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.

Equations

• Std.Time.TimeZone.Offset.fromOffset input = { config := { }, string := [Std.Time.FormatPart.modifier (Std.Time.Modifier.x Std.Time.OffsetX.hourMinuteColon)] }.parseBuilder some input

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

Formats a PlainDate using a specific format.

Equations

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

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.

Equations

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

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

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

Equations

• input.toAmericanDateString = Std.Time.Formats.americanDate.formatBuilder input.month input.day input.year

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.

Equations

• Std.Time.PlainDate.fromSQLDateString input = Std.Time.Formats.sqlDate.parseBuilder Std.Time.PlainDate.ofYearMonthDay? input

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

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

Equations

• input.toSQLDateString = Std.Time.Formats.sqlDate.formatBuilder input.year input.month input.day

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.

Equations

• Std.Time.PlainDate.fromLeanDateString input = Std.Time.Formats.leanDate.parseBuilder Std.Time.PlainDate.ofYearMonthDay? input

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

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

Equations

• input.toLeanDateString = Std.Time.Formats.leanDate.formatBuilder input.year input.month input.day

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

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

Equations

• Std.Time.PlainDate.parse input = (Std.Time.PlainDate.fromAmericanDateString input <|> Std.Time.PlainDate.fromSQLDateString input)

instance Std.Time.PlainDate.instToString : ToString PlainDate

Equations

• Std.Time.PlainDate.instToString = { toString := Std.Time.PlainDate.toLeanDateString }

instance Std.Time.PlainDate.instRepr : Repr PlainDate

Equations

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

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

Formats a PlainTime using a specific format.

Equations

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

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.

Equations

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

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

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

Equations

• input.toTime24Hour = Std.Time.Formats.time24Hour.formatBuilder input.hour input.minute input.second

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.

Equations

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

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

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

Equations

• input.toLeanTime24Hour = Std.Time.Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond

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.

Equations

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

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

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

Equations

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

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

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

Equations

• Std.Time.PlainTime.parse input = (Std.Time.PlainTime.fromTime12Hour input <|> Std.Time.PlainTime.fromTime24Hour input)

instance Std.Time.PlainTime.instToString : ToString PlainTime

Equations

• Std.Time.PlainTime.instToString = { toString := Std.Time.PlainTime.toLeanTime24Hour }

instance Std.Time.PlainTime.instRepr : Repr PlainTime

Equations

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

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

Formats a ZonedDateTime using a specific format.

Equations

• data.format format = match Std.Time.GenericFormat.spec format with | Except.error err => toString "error: " ++ toString err | Except.ok res => res.format data.toDateTime

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

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

Equations

• Std.Time.ZonedDateTime.fromISO8601String input = Std.Time.Formats.iso8601.parse input

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

Formats a ZonedDateTime value into an ISO8601 string.

Equations

• date.toISO8601String = Std.Time.Formats.iso8601.format date.toDateTime

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

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

Equations

• Std.Time.ZonedDateTime.fromRFC822String input = Std.Time.Formats.rfc822.parse input

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

Formats a ZonedDateTime value into an RFC822 format string.

Equations

• date.toRFC822String = Std.Time.Formats.rfc822.format date.toDateTime

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

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

Equations

• Std.Time.ZonedDateTime.fromRFC850String input = Std.Time.Formats.rfc850.parse input

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

Formats a ZonedDateTime value into an RFC850 format string.

Equations

• date.toRFC850String = Std.Time.Formats.rfc850.format date.toDateTime

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.

Equations

• Std.Time.ZonedDateTime.fromDateTimeWithZoneString input = Std.Time.Formats.dateTimeWithZone.parse input

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

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

Equations

• pdt.toDateTimeWithZoneString = Std.Time.Formats.dateTimeWithZone.format pdt.toDateTime

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.

Equations

• Std.Time.ZonedDateTime.fromLeanDateTimeWithZoneString input = (Std.Time.Formats.leanDateTimeWithZone.parse input <|> Std.Time.Formats.leanDateTimeWithZoneNoNanos.parse input)

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.

Equations

• Std.Time.ZonedDateTime.fromLeanDateTimeWithIdentifierString input = (Std.Time.Formats.leanDateTimeWithIdentifier.parse input <|> Std.Time.Formats.leanDateTimeWithIdentifierAndNanos.parse input)

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.

Equations

• zdt.toLeanDateTimeWithZoneString = Std.Time.Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset

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.

Equations

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

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

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

Equations

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

instance Std.Time.ZonedDateTime.instToString : ToString ZonedDateTime

Equations

• Std.Time.ZonedDateTime.instToString = { toString := Std.Time.ZonedDateTime.toLeanDateTimeWithIdentifierString }

instance Std.Time.ZonedDateTime.instRepr : Repr ZonedDateTime

Equations

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

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

Formats a PlainDateTime using a specific format.

Equations

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

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.

Equations

• Std.Time.PlainDateTime.fromAscTimeString input = Except.map Std.Time.DateTime.toPlainDateTime (Std.Time.Formats.ascTime.parse input)

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

Formats a PlainDateTime value into an AscTime format string.

Equations

• pdt.toAscTimeString = Std.Time.Formats.ascTime.format (Std.Time.DateTime.ofPlainDateTimeAssumingUTC pdt Std.Time.TimeZone.UTC)

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.

Equations

• Std.Time.PlainDateTime.fromLongDateFormatString input = Except.map Std.Time.DateTime.toPlainDateTime (Std.Time.Formats.longDateFormat.parse input)

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

Formats a PlainDateTime value into a LongDateFormat string.

Equations

• pdt.toLongDateFormatString = Std.Time.Formats.longDateFormat.format (Std.Time.DateTime.ofPlainDateTimeAssumingUTC pdt Std.Time.TimeZone.UTC)

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

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

Equations

• Std.Time.PlainDateTime.fromDateTimeString input = Except.map Std.Time.DateTime.toPlainDateTime (Std.Time.Formats.dateTime24Hour.parse input)

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

Formats a PlainDateTime value into a DateTime format string.

Equations

• pdt.toDateTimeString = Std.Time.Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond

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

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

Equations

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

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

Formats a PlainDateTime value into a DateTime format string.

Equations

• pdt.toLeanDateTimeString = Std.Time.Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond

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

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

Equations

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

instance Std.Time.PlainDateTime.instToString : ToString PlainDateTime

Equations

• Std.Time.PlainDateTime.instToString = { toString := Std.Time.PlainDateTime.toLeanDateTimeString }

instance Std.Time.PlainDateTime.instRepr : Repr PlainDateTime

Equations

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

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

Formats a DateTime using a specific format.

Equations

• data.format format = match Std.Time.GenericFormat.spec format with | Except.error err => toString "error: " ++ toString err | Except.ok res => res.format data

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.

Equations

• Std.Time.DateTime.fromAscTimeString input = Std.Time.Formats.ascTime.parse input

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

Formats a DateTime value into an AscTime format string.

Equations

• datetime.toAscTimeString = Std.Time.Formats.ascTime.format datetime

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.

Equations

• Std.Time.DateTime.fromLongDateFormatString input = Std.Time.Formats.longDateFormat.parse input

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

Formats a DateTime value into a LongDateFormat string.

Equations

• datetime.toLongDateFormatString = Std.Time.Formats.longDateFormat.format datetime

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

Formats a DateTime value into an ISO8601 string.

Equations

• date.toISO8601String = Std.Time.Formats.iso8601.format date

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

Formats a DateTime value into an RFC822 format string.

Equations

• date.toRFC822String = Std.Time.Formats.rfc822.format date

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

Formats a DateTime value into an RFC850 format string.

Equations

• date.toRFC850String = Std.Time.Formats.rfc850.format date

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

Formats a DateTime value into a DateTimeWithZone format string.

Equations

• pdt.toDateTimeWithZoneString = Std.Time.Formats.dateTimeWithZone.format pdt

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

Equations

• pdt.toLeanDateTimeWithZoneString = Std.Time.Formats.leanDateTimeWithZone.format pdt

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.

Equations

• Std.Time.DateTime.parse date = (Std.Time.DateTime.fromAscTimeString date <|> Std.Time.DateTime.fromLongDateFormatString date)

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

Equations

• Std.Time.DateTime.instRepr = { reprPrec := fun (data : Std.Time.DateTime tz) => Repr.addAppParen (Std.Format.text data.toLeanDateTimeWithZoneString) }

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

Equations

• Std.Time.DateTime.instToString = { toString := Std.Time.DateTime.toLeanDateTimeWithZoneString }