def Std.Time.«termZoned(_)» : Lean.ParserDescr

Defines a syntax for zoned datetime values. It expects a string representing a datetime with timezone information.

Example: zoned("2024-10-13T15:00:00-03:00")

def Std.Time.«termZoned(_,_)» : Lean.ParserDescr

Defines a syntax for zoned datetime values. It expects a string representing a datetime and a timezone information as a term.

Example: zoned("2024-10-13T15:00:00", timezone)

def Std.Time.«termDatetime(_)» : Lean.ParserDescr

Defines a syntax for datetime values without timezone. The input should be a string in an ISO8601-like format.

Example: datetime("2024-10-13T15:00:00")

def Std.Time.«termDate(_)» : Lean.ParserDescr

Defines a syntax for date-only values. The input string represents a date in formats like "YYYY-MM-DD".

Example: date("2024-10-13")

Equations

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

def Std.Time.«termTime(_)» : Lean.ParserDescr

Defines a syntax for time-only values. The string should represent a time, either in 24-hour or 12-hour format.

Example: time("15:00:00") or time("03:00:00 PM")

def Std.Time.«termOffset(_)» : Lean.ParserDescr

Defines a syntax for UTC offset values. The string should indicate the time difference from UTC (e.g., "-03:00").

Example: offset("-03:00")

def Std.Time.«termTimezone(_)» : Lean.ParserDescr

Defines a syntax for timezone identifiers. The input string should be a valid timezone name or abbreviation.

Example: timezone("America/Sao_Paulo")

Equations

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