def Time.parse {α : Type} {m : Type → Type v} [Monad m] [Time.MonadFail m α] [Time.ParseTime α] (l : Time.TimeLocale) (fmt s : String) : m α

Parses a time value (i.e. instance of ParseTime) given a format string (Time.Specifier)

Equations

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

def String.toZonedTime? (l : Time.TimeLocale) (s : String) : Option Time.ZonedTime

parse ZonedTime value from ISO 8601 string, e.g. '2023-02-02T19:55:03+01:00'

Equations

• String.toZonedTime? l s = Time.parse l "%Y-%m-%dT%H:%M:%S%Q%Ez" s