inductive Lean.Parsec.ParseResult (α : Type) : Type

• success: {α : Type} → String.Iterator → α → Lean.Parsec.ParseResult α
• error: {α : Type} → String.Iterator → String → Lean.Parsec.ParseResult α

instance Lean.Parsec.instReprParseResult : {α : Type} → [inst : Repr α] → Repr (Lean.Parsec.ParseResult α)

Equations

• Lean.Parsec.instReprParseResult = { reprPrec := Lean.Parsec.reprParseResult✝ }

def Lean.Parsec (α : Type) : Type

Equations

• Lean.Parsec α = (String.Iterator → Lean.Parsec.ParseResult α)

instance Lean.Parsec.instInhabited (α : Type) : Inhabited (Lean.Parsec α)

Equations

• Lean.Parsec.instInhabited α = { default := fun (it : String.Iterator) => Lean.Parsec.ParseResult.error it "" }

@[inline]

def Lean.Parsec.pure {α : Type} (a : α) : Lean.Parsec α

Equations

• Lean.Parsec.pure a it = Lean.Parsec.ParseResult.success it a

@[inline]

def Lean.Parsec.bind {α : Type} {β : Type} (f : Lean.Parsec α) (g : α → Lean.Parsec β) : Lean.Parsec β

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

instance Lean.Parsec.instMonad : Monad Lean.Parsec

Equations

• Lean.Parsec.instMonad = Monad.mk

@[inline]

def Lean.Parsec.fail {α : Type} (msg : String) : Lean.Parsec α

Equations

• Lean.Parsec.fail msg it = Lean.Parsec.ParseResult.error it msg

@[inline]

def Lean.Parsec.tryCatch {α : Type} {β : Type} (p : Lean.Parsec α) (csuccess : α → Lean.Parsec β) (cerror : Unit → Lean.Parsec β) : Lean.Parsec β

Equations

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

@[inline]

def Lean.Parsec.orElse {α : Type} (p : Lean.Parsec α) (q : Unit → Lean.Parsec α) : Lean.Parsec α

Equations

• p.orElse q = p.tryCatch pure q

@[inline]

def Lean.Parsec.attempt {α : Type} (p : Lean.Parsec α) : Lean.Parsec α

Equations

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

instance Lean.Parsec.instAlternative : Alternative Lean.Parsec

Equations

• Lean.Parsec.instAlternative = Alternative.mk (fun {α : Type} => Lean.Parsec.fail "") fun {α : Type} => Lean.Parsec.orElse

def Lean.Parsec.run {α : Type} (p : Lean.Parsec α) (s : String) : Except String α

Equations

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

def Lean.Parsec.expectedEndOfInput : String

Equations

• Lean.Parsec.expectedEndOfInput = "expected end of input"

@[inline]

def Lean.Parsec.eof : Lean.Parsec Unit

Equations

• Lean.Parsec.eof it = if it.hasNext = true then Lean.Parsec.ParseResult.error it Lean.Parsec.expectedEndOfInput else Lean.Parsec.ParseResult.success it ()

@[specialize #[]]

partial def Lean.Parsec.manyCore {α : Type} (p : Lean.Parsec α) (acc : Array α) : Lean.Parsec (Array α)

@[inline]

def Lean.Parsec.many {α : Type} (p : Lean.Parsec α) : Lean.Parsec (Array α)

Equations

• p.many = p.manyCore #[]

@[inline]

def Lean.Parsec.many1 {α : Type} (p : Lean.Parsec α) : Lean.Parsec (Array α)

Equations

• p.many1 = do let __do_lift ← p p.manyCore #[__do_lift]

@[specialize #[]]

partial def Lean.Parsec.manyCharsCore (p : Lean.Parsec Char) (acc : String) : Lean.Parsec String

@[inline]

def Lean.Parsec.manyChars (p : Lean.Parsec Char) : Lean.Parsec String

Equations

• p.manyChars = p.manyCharsCore ""

@[inline]

def Lean.Parsec.many1Chars (p : Lean.Parsec Char) : Lean.Parsec String

Equations

• p.many1Chars = do let __do_lift ← p p.manyCharsCore __do_lift.toString

def Lean.Parsec.pstring (s : String) : Lean.Parsec String

Parses the given string.

Equations

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

@[inline]

def Lean.Parsec.skipString (s : String) : Lean.Parsec Unit

Equations

• Lean.Parsec.skipString s = SeqRight.seqRight (Lean.Parsec.pstring s) fun (x : Unit) => pure ()

def Lean.Parsec.unexpectedEndOfInput : String

Equations

• Lean.Parsec.unexpectedEndOfInput = "unexpected end of input"

@[inline]

def Lean.Parsec.anyChar : Lean.Parsec Char

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

@[inline]

def Lean.Parsec.pchar (c : Char) : Lean.Parsec Char

Equations

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

@[inline]

def Lean.Parsec.skipChar (c : Char) : Lean.Parsec Unit

Equations

• Lean.Parsec.skipChar c = SeqRight.seqRight (Lean.Parsec.pchar c) fun (x : Unit) => pure ()

@[inline]

def Lean.Parsec.digit : Lean.Parsec Char

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

@[inline]

def Lean.Parsec.hexDigit : Lean.Parsec Char

Equations

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

@[inline]

def Lean.Parsec.asciiLetter : Lean.Parsec Char

Equations

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

@[inline]

def Lean.Parsec.satisfy (p : Char → Bool) : Lean.Parsec Char

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

@[inline]

def Lean.Parsec.notFollowedBy {α : Type} (p : Lean.Parsec α) : Lean.Parsec Unit

Equations

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

partial def Lean.Parsec.skipWs (it : String.Iterator) : String.Iterator

@[inline]

def Lean.Parsec.peek? : Lean.Parsec (Option Char)

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

@[inline]

def Lean.Parsec.peek! : Lean.Parsec Char

Equations

• Lean.Parsec.peek! = do let __discr ← Lean.Parsec.peek? match __discr with | some c => pure c | x => Lean.Parsec.fail Lean.Parsec.unexpectedEndOfInput

@[inline]

def Lean.Parsec.skip : Lean.Parsec Unit

Equations

• Lean.Parsec.skip it = Lean.Parsec.ParseResult.success it.next ()

@[inline]

def Lean.Parsec.ws : Lean.Parsec Unit

Equations

• Lean.Parsec.ws it = Lean.Parsec.ParseResult.success (Lean.Parsec.skipWs it) ()