def Parsec.count {α : Type} (n : Nat) (p : Std.Internal.Parsec.String.Parser α) : Std.Internal.Parsec.String.Parser (List α)

Equations

• Parsec.count n p = List.mapM id (List.replicate n p)

def Parsec.choice {α : Type} : List (Std.Internal.Parsec.String.Parser α) → Std.Internal.Parsec.String.Parser α

Equations

• Parsec.choice [] = Std.Internal.Parsec.fail ""
• Parsec.choice [p] = p
• Parsec.choice (p :: ps) = (Std.Internal.Parsec.attempt p <|> Parsec.choice ps)

def Parsec.toNat (chars : List Char) : Nat

Equations

• Parsec.toNat chars = List.foldl (fun (acc : Nat) (c : Char) => 10 * acc + (c.val.toNat - '0'.val.toNat)) 0 chars

def Parsec.nat (n : Nat) : Std.Internal.Parsec.String.Parser Nat

Equations

• Parsec.nat n = do let __do_lift ← Parsec.count n Std.Internal.Parsec.String.digit pure (Parsec.toNat __do_lift)

def Parsec.digits (n : Nat) : Std.Internal.Parsec.String.Parser String

Equations

• Parsec.digits n = do let __do_lift ← Parsec.count n Std.Internal.Parsec.String.digit pure __do_lift.asString

def Parsec.allowChar (c : Char) : Std.Internal.Parsec.String.Parser String

Equations

• Parsec.allowChar c = ((fun (x : Char) => x.toString) <$> Std.Internal.Parsec.String.pchar c <|> pure "")

instance Time.instMonadFailOption (α : Type) : Time.MonadFail Option α

Equations

• Time.instMonadFailOption α = { fail := fun (x : String) => none }

instance Time.instMonadFailParser (α : Type) : Time.MonadFail Std.Internal.Parsec.String.Parser α

Equations

• Time.instMonadFailParser α = { fail := fun (s : String) (it : String.Iterator) => Std.Internal.Parsec.ParseResult.error it s }

instance Time.instReadMaybeString : Time.ReadMaybe String

Equations

• Time.instReadMaybeString = { readMaybe := fun (s : String) => some s }

instance Time.instReadMaybeInt : Time.ReadMaybe Int

Equations

• Time.instReadMaybeInt = { readMaybe := fun (s : String) => s.toInt? }

inductive Time.PaddingSide : Type

• PrePadding: Time.PaddingSide
• PostPadding: Time.PaddingSide

inductive Time.WeekType : Type

• ISOWeek: Time.WeekType
• SundayWeek: Time.WeekType
• MondayWeek: Time.WeekType

instance Time.instReprWeekType : Repr Time.WeekType

Equations

• Time.instReprWeekType = { reprPrec := Time.reprWeekType✝ }

instance Time.instBEqWeekType : BEq Time.WeekType

Equations

• Time.instBEqWeekType = { beq := Time.beqWeekType✝ }

inductive Time.DayComponent : Type

• DCCentury: Int → Time.DayComponent
• DCCenturyYear: Int → Time.DayComponent
• DCYearMonth: Int → Time.DayComponent
• DCMonthDay: Int → Time.DayComponent
• DCYearDay: Int → Time.DayComponent
• DCWeekDay: Int → Time.DayComponent
• DCYearWeek: Time.WeekType → Int → Time.DayComponent

instance Time.instReprDayComponent : Repr Time.DayComponent

Equations

• Time.instReprDayComponent = { reprPrec := Time.reprDayComponent✝ }

instance Time.instBEqDayComponent : BEq Time.DayComponent

Equations

• Time.instBEqDayComponent = { beq := Time.beqDayComponent✝ }

def Time.DCCentury? : Time.DayComponent → Option Int

Equations

• Time.DCCentury? (Time.DayComponent.DCCentury y) = some y
• Time.DCCentury? x = none

def Time.DCCenturyYear? : Time.DayComponent → Option Int

Equations

• Time.DCCenturyYear? (Time.DayComponent.DCCenturyYear y) = some y
• Time.DCCenturyYear? x = none

def Time.DCYearMonth? : Time.DayComponent → Option Int

Equations

• Time.DCYearMonth? (Time.DayComponent.DCYearMonth y) = some y
• Time.DCYearMonth? x = none

def Time.DCMonthDay? : Time.DayComponent → Option Int

Equations

• Time.DCMonthDay? (Time.DayComponent.DCMonthDay y) = some y
• Time.DCMonthDay? x = none

def Time.DCYearDay? : Time.DayComponent → Option Int

Equations

• Time.DCYearDay? (Time.DayComponent.DCYearDay y) = some y
• Time.DCYearDay? x = none

def Time.DCWeekDay? : Time.DayComponent → Option Int

Equations

• Time.DCWeekDay? (Time.DayComponent.DCWeekDay y) = some y
• Time.DCWeekDay? x = none

def Time.DCYearWeek? : Time.WeekType → Time.DayComponent → Option Int

Equations

• Time.DCYearWeek? Time.WeekType.ISOWeek (Time.DayComponent.DCYearWeek Time.WeekType.ISOWeek y) = some y
• Time.DCYearWeek? Time.WeekType.SundayWeek (Time.DayComponent.DCYearWeek Time.WeekType.SundayWeek y) = some y
• Time.DCYearWeek? Time.WeekType.MondayWeek (Time.DayComponent.DCYearWeek Time.WeekType.MondayWeek y) = some y
• Time.DCYearWeek? x✝ x = none

def Time.allowEmptyParser : Bool → Std.Internal.Parsec.String.Parser String

Equations

• Time.allowEmptyParser false = do let x ← Std.Internal.Parsec.many1 Std.Internal.Parsec.String.digit pure x.toList.asString
• Time.allowEmptyParser true = do let x ← Std.Internal.Parsec.many Std.Internal.Parsec.String.digit pure x.toList.asString

def Time.parsePaddedDigits : Time.PaddingSide → Time.ParseNumericPadding → Bool → Nat → Std.Internal.Parsec.String.Parser String

Equations

• Time.parsePaddedDigits x✝¹ Time.ParseNumericPadding.ZeroPadding x✝ x = do let x ← Parsec.count x Std.Internal.Parsec.String.digit pure x.asString
• Time.parsePaddedDigits Time.PaddingSide.PrePadding Time.ParseNumericPadding.SpacePadding x✝ x = Std.Internal.Parsec.String.ws *> Time.allowEmptyParser x✝
• Time.parsePaddedDigits Time.PaddingSide.PostPadding Time.ParseNumericPadding.SpacePadding x✝ x = Time.allowEmptyParser x✝ <* Std.Internal.Parsec.String.ws
• Time.parsePaddedDigits x✝ Time.ParseNumericPadding.NoPadding false x = do let x ← Std.Internal.Parsec.many1 Std.Internal.Parsec.String.digit pure x.toList.asString
• Time.parsePaddedDigits x✝ Time.ParseNumericPadding.NoPadding true x = do let x ← Std.Internal.Parsec.many Std.Internal.Parsec.String.digit pure x.toList.asString

def Time.timeParseTimeSpecifier (l : Time.TimeLocale) (mpad : Option Time.ParseNumericPadding) (s : Time.Specifier) : Std.Internal.Parsec.String.Parser String

Equations

• One or more equations did not get rendered due to their size.
• Time.timeParseTimeSpecifier l mpad Time.Specifier.C = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.f = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.Y = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.ZeroPadding 4
• Time.timeParseTimeSpecifier l mpad Time.Specifier.G = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 4
• Time.timeParseTimeSpecifier l mpad Time.Specifier.y = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.g = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.B = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.fst) l.months)
• Time.timeParseTimeSpecifier l mpad Time.Specifier.b = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.snd) l.months)
• Time.timeParseTimeSpecifier l mpad Time.Specifier.m = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.d = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.e = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.SpacePadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.V = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.U = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.W = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.u = Time.timeParseTimeSpecifier.oneOf (List.map toString [1, 2, 3, 4, 5, 6, 7])
• Time.timeParseTimeSpecifier l mpad Time.Specifier.A = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.fst) l.wDays)
• Time.timeParseTimeSpecifier l mpad Time.Specifier.a = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.snd) l.wDays)
• Time.timeParseTimeSpecifier l mpad Time.Specifier.w = Time.timeParseTimeSpecifier.oneOf (List.map toString [0, 1, 2, 3, 4, 5, 6])
• Time.timeParseTimeSpecifier l mpad Time.Specifier.j = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 3
• Time.timeParseTimeSpecifier l mpad Time.Specifier.H = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.M = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.S = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
• Time.timeParseTimeSpecifier l mpad Time.Specifier.q = Time.timeParseTimeSpecifier.digits' mpad Time.PaddingSide.PostPadding Time.ParseNumericPadding.ZeroPadding true Time.Nano
• Time.timeParseTimeSpecifier l mpad Time.Specifier.z = Time.timeParseTimeSpecifier.numericTZ mpad
• Time.timeParseTimeSpecifier l mpad Time.Specifier.Ez = Time.timeParseTimeSpecifier.numericTZ mpad
• Time.timeParseTimeSpecifier l mpad Time.Specifier.Z = Time.timeParseTimeSpecifier.numericTZ mpad
• Time.timeParseTimeSpecifier l mpad Time.Specifier.EZ = Time.timeParseTimeSpecifier.numericTZ mpad
• Time.timeParseTimeSpecifier l mpad Time.Specifier.l = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
• Time.timeParseTimeSpecifier l mpad Time.Specifier.I = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
• Time.timeParseTimeSpecifier l mpad Time.Specifier.k = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
• Time.timeParseTimeSpecifier l mpad Time.Specifier.p = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
• Time.timeParseTimeSpecifier l mpad Time.Specifier.P = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")

def Time.timeParseTimeSpecifier.digits' (mpad : Option Time.ParseNumericPadding) (ps : Time.PaddingSide) (pad : Time.ParseNumericPadding) (allowEmpty : Bool) (n : Nat) : Std.Internal.Parsec.String.Parser String

Equations

• Time.timeParseTimeSpecifier.digits' mpad ps pad allowEmpty n = Time.parsePaddedDigits ps (mpad.getD pad) allowEmpty n

def Time.timeParseTimeSpecifier.digits (mpad : Option Time.ParseNumericPadding) (pad : Time.ParseNumericPadding) (n : Nat) : Std.Internal.Parsec.String.Parser String

Equations

• Time.timeParseTimeSpecifier.digits mpad pad n = Time.timeParseTimeSpecifier.digits' mpad Time.PaddingSide.PrePadding pad false n

def Time.timeParseTimeSpecifier.allowNegativeDigits (mpad : Option Time.ParseNumericPadding) (pad : Time.ParseNumericPadding) (n : Nat) : Std.Internal.Parsec.String.Parser String

Equations

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

def Time.timeParseTimeSpecifier.oneOf (l : List String) : Std.Internal.Parsec.String.Parser String

Equations

• Time.timeParseTimeSpecifier.oneOf l = Parsec.choice (List.map (fun (x : String) => Std.Internal.Parsec.String.pstring x) l)

def Time.timeParseTimeSpecifier.numericTZ (mpad : Option Time.ParseNumericPadding) : Std.Internal.Parsec.String.Parser String

Equations

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

def Time.timeSubstituteTimeSpecifier : Time.TimeLocale → Time.SubstituteSpecifier → String

Equations

• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.c = x.dateTimeFmt
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.R = "%H:%M"
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.T = "%H:%M:%S"
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.X = x.timeFmt
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.r = x.time12Fmt
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.D = "%m/%d/%y"
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.F = "%Y-%m-%d"
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.x = x.dateFmt
• Time.timeSubstituteTimeSpecifier x Time.SubstituteSpecifier.h = "%b"

def Time.makeDayComponent (l : Time.TimeLocale) (c : Time.Specifier) (s : String) : Option (List Time.DayComponent)

def Time.makeDayComponent.indexOf? {α : Type} (p : α → Bool) (l : List α) : Option Int

Equations

• Time.makeDayComponent.indexOf? p l = match List.find? (fun (x : Nat × α) => p x.snd) l.enum with | some (i, snd) => some ↑i | x => none

def Time.makeDayComponents (l : Time.TimeLocale) (pairs : List (Time.Specifier × String)) : Option (List Time.DayComponent)

Equations

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

def Time.makeDayComponents.flatten {α : Type} (l : List (List α)) : List α

Equations

• Time.makeDayComponents.flatten l = List.foldr (fun (c acc : List α) => c ++ acc) [] l

def Time.safeLast {α : Type} (a : α) (l : List α) : α

Equations

• Time.safeLast a l = (a :: l).getLast ⋯

instance Time.instParseTimeDay : Time.ParseTime Time.Day

Equations

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

def Time.instParseTimeDay.year (cs : List Time.DayComponent) : Int

Equations

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

def Time.instParseTimeDay.rest : List Time.DayComponent → List Time.DayComponent → Option Time.Day

Equations

• One or more equations did not get rendered due to their size.
• Time.instParseTimeDay.rest x (Time.DayComponent.DCYearMonth m :: tail) = Time.fromGregorianValid (Time.instParseTimeDay.year x) m (Time.safeLast 1 (List.filterMap Time.DCMonthDay? x))
• Time.instParseTimeDay.rest x (Time.DayComponent.DCYearDay yd :: tail) = Time.fromOrdinalDateValid (Time.instParseTimeDay.year x) yd
• Time.instParseTimeDay.rest x (head :: xs) = Time.instParseTimeDay.rest x xs
• Time.instParseTimeDay.rest x [] = none

instance Time.instParseTimeDate : Time.ParseTime Time.Date

Equations

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

instance Time.instParseTimeTimeOfDay : Time.ParseTime Time.TimeOfDay

Equations

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

def Time.instParseTimeTimeOfDay.f (tod : Time.TimeOfDay) (pair : Time.Specifier × String) : Option Time.TimeOfDay

Equations

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

instance Time.instParseTimeLocalTime : Time.ParseTime Time.LocalTime

Equations

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

def Time.readTzOffset (s : String) : Option Int

Equations

• Time.readTzOffset s = match s.toList with | [s, h1, h2, m1, m2] => Time.readTzOffset.calculate s h1 h2 m1 m2 | x => none

def Time.readTzOffset.getSign : Char → Option Int

Equations

• Time.readTzOffset.getSign '+' = some 1
• Time.readTzOffset.getSign '-' = some (-1)
• Time.readTzOffset.getSign x = none

def Time.readTzOffset.calculate (s h1 h2 m1 m2 : Char) : Option Int

Equations

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

instance Time.instParseTimeTimeZone : Time.ParseTime Time.TimeZone

Equations

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

def Time.instParseTimeTimeZone.f (tz : Time.TimeZone) (pair : Time.Specifier × String) : Option Time.TimeZone

Equations

• Time.instParseTimeTimeZone.f tz (Time.Specifier.z, s) = do let offset ← Time.readTzOffset s pure { timeZoneMinutes := offset, timeZoneSummerOnly := false, timeZoneName := "" }
• Time.instParseTimeTimeZone.f tz pair = some tz

instance Time.instParseTimeZonedTime : Time.ParseTime Time.ZonedTime

Equations

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