def Parsec.count {α : Type} (n : Nat) (p : Lean.Parsec α) : Lean.Parsec (List α)

Equations

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

def Parsec.choice {α : Type} : List (Lean.Parsec α) → Lean.Parsec α

Equations

• Parsec.choice [] = Lean.Parsec.fail ""
• Parsec.choice [p] = p
• Parsec.choice (p :: ps) = HOrElse.hOrElse p.attempt fun (x : Unit) => 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) : Lean.Parsec Nat

Equations

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

def Parsec.digits (n : Nat) : Lean.Parsec String

Equations

• Parsec.digits n = do let __do_lift ← Parsec.count n Lean.Parsec.digit pure __do_lift.asString

def Parsec.allowChar (c : Char) : Lean.Parsec String

Equations

• Parsec.allowChar c = HOrElse.hOrElse ((fun (x : Char) => x.toString) <$> Lean.Parsec.pchar c) fun (x : Unit) => pure ""

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

Equations

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

instance Time.instMonadFailParsec (α : Type) : Time.MonadFail Lean.Parsec α

Equations

• Time.instMonadFailParsec α = { fail := fun (s : String) (it : String.Iterator) => Lean.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? x = match x with | Time.DayComponent.DCCentury y => some y | x => none

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

Equations

• Time.DCCenturyYear? x = match x with | Time.DayComponent.DCCenturyYear y => some y | x => none

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

Equations

• Time.DCYearMonth? x = match x with | Time.DayComponent.DCYearMonth y => some y | x => none

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

Equations

• Time.DCMonthDay? x = match x with | Time.DayComponent.DCMonthDay y => some y | x => none

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

Equations

• Time.DCYearDay? x = match x with | Time.DayComponent.DCYearDay y => some y | x => none

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

Equations

• Time.DCWeekDay? x = match x with | Time.DayComponent.DCWeekDay y => some y | x => none

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

Equations

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

def Time.allowEmptyParser : Bool → Lean.Parsec String

Equations

• Time.allowEmptyParser x = match x with | false => do let x ← Lean.Parsec.digit.many1 pure x.toList.asString | true => do let x ← Lean.Parsec.digit.many pure x.toList.asString

def Time.parsePaddedDigits : Time.PaddingSide → Time.ParseNumericPadding → Bool → Nat → Lean.Parsec String

Equations

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

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

Equations

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

def Time.timeParseTimeSpecifier.digits' (mpad : Option Time.ParseNumericPadding) (ps : Time.PaddingSide) (pad : Time.ParseNumericPadding) (allowEmpty : Bool) (n : Nat) : Lean.Parsec 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) : Lean.Parsec 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) : Lean.Parsec String

Equations

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

def Time.timeParseTimeSpecifier.oneOf (l : List String) : Lean.Parsec String

Equations

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

def Time.timeParseTimeSpecifier.numericTZ (mpad : Option Time.ParseNumericPadding) : Lean.Parsec String

Equations

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

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

Equations

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

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

Equations

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

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) = let md := Time.safeLast 1 (List.filterMap Time.DCMonthDay? x); Time.fromGregorianValid (Time.instParseTimeDay.year x) m md
• 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 x = match x with | '+' => some 1 | '-' => some (-1) | x => none

def Time.readTzOffset.calculate (s : Char) (h1 : Char) (h2 : Char) (m1 : Char) (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

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

instance Time.instParseTimeZonedTime : Time.ParseTime Time.ZonedTime

Equations

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