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 : ParseNumericPadding
• SpacePadding : ParseNumericPadding
• ZeroPadding : ParseNumericPadding

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

• substituteTimeSpecifier : TimeLocale → SubstituteSpecifier → String
• parseTimeSpecifier : TimeLocale → Option ParseNumericPadding → Specifier → Std.Internal.Parsec.String.Parser String
• buildTime : TimeLocale → List (Specifier × String) → Option α

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

Equations

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

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

Equations

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