- success: {α : Type} → String.Iterator → α → Lean.Parsec.ParseResult α
- error: {α : Type} → String.Iterator → String → Lean.Parsec.ParseResult α
Instances For
instance
Lean.Parsec.instReprParseResult :
{α : Type} → [inst : Repr α] → Repr (Lean.Parsec.ParseResult α)
Equations
- Lean.Parsec.instReprParseResult = { reprPrec := Lean.Parsec.reprParseResult✝ }
Equations
Instances For
Equations
- Lean.Parsec.instInhabited α = { default := fun (it : String.Iterator) => Lean.Parsec.ParseResult.error it "" }
@[inline]
Equations
- f.bind g it = match f it with | Lean.Parsec.ParseResult.success rem a => g a rem | Lean.Parsec.ParseResult.error pos msg => Lean.Parsec.ParseResult.error pos msg
Instances For
@[inline]
def
Lean.Parsec.tryCatch
{α : Type}
{β : Type}
(p : Lean.Parsec α)
(csuccess : α → Lean.Parsec β)
(cerror : Unit → Lean.Parsec β)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parsec.instAlternative = Alternative.mk (fun {α : Type} => Lean.Parsec.fail "") fun {α : Type} => Lean.Parsec.orElse
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parsec.expectedEndOfInput = "expected end of input"
Instances For
@[inline]
Equations
- Lean.Parsec.eof it = if it.hasNext = true then Lean.Parsec.ParseResult.error it Lean.Parsec.expectedEndOfInput else Lean.Parsec.ParseResult.success it ()
Instances For
@[specialize #[]]
partial def
Lean.Parsec.manyCore
{α : Type}
(p : Lean.Parsec α)
(acc : Array α)
:
Lean.Parsec (Array α)
@[specialize #[]]
@[inline]
Equations
- p.many1Chars = do let __do_lift ← p p.manyCharsCore __do_lift.toString
Instances For
Parses the given string.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
- Lean.Parsec.skipString s = SeqRight.seqRight (Lean.Parsec.pstring s) fun (x : Unit) => pure ()
Instances For
Equations
- Lean.Parsec.unexpectedEndOfInput = "unexpected end of input"
Instances For
@[inline]
Equations
- Lean.Parsec.anyChar it = if it.hasNext = true then Lean.Parsec.ParseResult.success it.next it.curr else Lean.Parsec.ParseResult.error it Lean.Parsec.unexpectedEndOfInput
Instances For
@[inline]
Equations
- Lean.Parsec.pchar c = (do let __do_lift ← Lean.Parsec.anyChar if __do_lift = c then pure c else Lean.Parsec.fail (toString "expected: '" ++ toString c ++ toString "'")).attempt
Instances For
@[inline]
Equations
- Lean.Parsec.skipChar c = SeqRight.seqRight (Lean.Parsec.pchar c) fun (x : Unit) => pure ()
Instances For
@[inline]
Equations
- Lean.Parsec.digit = (do let c ← Lean.Parsec.anyChar if '0' ≤ c ∧ c ≤ '9' then pure c else Lean.Parsec.fail (toString "digit expected")).attempt
Instances For
@[inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
- Lean.Parsec.asciiLetter = (do let c ← Lean.Parsec.anyChar if 'A' ≤ c ∧ c ≤ 'Z' ∨ 'a' ≤ c ∧ c ≤ 'z' then pure c else Lean.Parsec.fail (toString "ASCII letter expected")).attempt
Instances For
@[inline]
Equations
- Lean.Parsec.satisfy p = (do let c ← Lean.Parsec.anyChar if p c = true then pure c else Lean.Parsec.fail "condition not satisfied").attempt
Instances For
@[inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
- Lean.Parsec.peek? it = if it.hasNext = true then Lean.Parsec.ParseResult.success it (some it.curr) else Lean.Parsec.ParseResult.success it none
Instances For
@[inline]
Equations
- Lean.Parsec.peek! = do let __discr ← Lean.Parsec.peek? match __discr with | some c => pure c | x => Lean.Parsec.fail Lean.Parsec.unexpectedEndOfInput
Instances For
@[inline]