inductive Std.Internal.Parsec.ParseResult (α ι : Type) : Type

• success {α ι : Type} (pos : ι) (res : α) : ParseResult α ι
• error {α ι : Type} (pos : ι) (err : String) : ParseResult α ι

instance Std.Internal.Parsec.instReprParseResult {α✝ ι✝ : Type} [Repr α✝] [Repr ι✝] : Repr (ParseResult α✝ ι✝)

def Std.Internal.Parsec (ι α : Type) : Type

class Std.Internal.Parsec.Input (ι : Type) (elem idx : outParam Type) [DecidableEq idx] [DecidableEq elem] : Type

• pos : ι → idx
• next : ι → ι
• curr : ι → elem
• hasNext : ι → Bool
• next' (it : ι) : hasNext it = true → ι
• curr' (it : ι) : hasNext it = true → elem

instance Std.Internal.Parsec.instInhabited {α ι : Type} : Inhabited (Parsec ι α)

@[inline]

def Std.Internal.Parsec.pure {α ι : Type} (a : α) : Parsec ι α

@[inline]

def Std.Internal.Parsec.bind {ι α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β

@[always_inline]

instance Std.Internal.Parsec.instMonad {ι : Type} : Monad (Parsec ι)

@[inline]

def Std.Internal.Parsec.fail {α ι : Type} (msg : String) : Parsec ι α

@[inline]

def Std.Internal.Parsec.tryCatch {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] {β : Type} (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit → Parsec ι β) : Parsec ι β

@[inline]

def Std.Internal.Parsec.orElse {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (q : Unit → Parsec ι α) : Parsec ι α

@[inline]

def Std.Internal.Parsec.attempt {α ι : Type} (p : Parsec ι α) : Parsec ι α

@[always_inline]

instance Std.Internal.Parsec.instAlternative {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Alternative (Parsec ι)

def Std.Internal.Parsec.expectedEndOfInput : String

@[inline]

def Std.Internal.Parsec.eof {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι Unit

@[inline]

def Std.Internal.Parsec.isEof {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι Bool

@[specialize #[]]

partial def Std.Internal.Parsec.manyCore {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (acc : Array α) : Parsec ι (Array α)

@[inline]

def Std.Internal.Parsec.many {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) : Parsec ι (Array α)

@[inline]

def Std.Internal.Parsec.many1 {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) : Parsec ι (Array α)

def Std.Internal.Parsec.unexpectedEndOfInput : String

@[inline]

def Std.Internal.Parsec.any {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι elem

@[inline]

def Std.Internal.Parsec.satisfy {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : elem → Bool) : Parsec ι elem

@[inline]

def Std.Internal.Parsec.notFollowedBy {α ι : Type} (p : Parsec ι α) : Parsec ι Unit

@[inline]

def Std.Internal.Parsec.peek? {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι (Option elem)

@[inline]

def Std.Internal.Parsec.peek! {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι elem

@[inline]

def Std.Internal.Parsec.peekD {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (default : elem) : Parsec ι elem

@[inline]

def Std.Internal.Parsec.skip {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] : Parsec ι Unit

@[specialize #[]]

partial def Std.Internal.Parsec.manyCharsCore {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) (acc : String) : Parsec ι String

@[inline]

def Std.Internal.Parsec.manyChars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) : Parsec ι String

@[inline]

def Std.Internal.Parsec.many1Chars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) : Parsec ι String