class Time.ReadMaybe (α : Type u) [Repr α] [BEq α] : Type u

• readMaybe : String → Option α

class Time.MonadFail (m : Type u → Type v) (α : Type u) : Type v

• fail : String → m α

inductive Time.ParseNumericPadding : Type

• NoPadding: Time.ParseNumericPadding
• SpacePadding: Time.ParseNumericPadding
• ZeroPadding: Time.ParseNumericPadding

class Time.ParseTime (α : Type u) : Type u

• substituteTimeSpecifier : Time.TimeLocale → Time.SubstituteSpecifier → String
• parseTimeSpecifier : Time.TimeLocale → Option Time.ParseNumericPadding → Time.Specifier → Lean.Parsec String
• buildTime : Time.TimeLocale → List (Time.Specifier × String) → Option α

def Time.parseSpecifiers (α : Type u) [Time.ParseTime α] (l : Time.TimeLocale) (fmt : String) : Lean.Parsec (List (Time.Specifier × String))

Equations

• Time.parseSpecifiers α l fmt = Time.parse α l fmt.toList

def Time.parseTime {α : Type} [Time.ParseTime α] (l : Time.TimeLocale) (fmt : String) : Lean.Parsec α

Equations

• Time.parseTime l fmt = do let pairs ← Time.parseSpecifiers α l fmt match Time.ParseTime.buildTime l pairs with | some t => pure t | none => Lean.Parsec.fail ""