@[inline]

def Lean.Json.Parser.hexChar : Lean.Parsec Nat

def Lean.Json.Parser.escapedChar : Lean.Parsec Char

partial def Lean.Json.Parser.strCore (acc : String) : Lean.Parsec String

def Lean.Json.Parser.str : Lean.Parsec String

partial def Lean.Json.Parser.natCore (acc : Nat) (digits : Nat) : Lean.Parsec (Nat × Nat)

@[inline]

def Lean.Json.Parser.lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Lean.Parsec Unit

@[inline]

def Lean.Json.Parser.natNonZero : Lean.Parsec Nat

@[inline]

def Lean.Json.Parser.natNumDigits : Lean.Parsec (Nat × Nat)

@[inline]

def Lean.Json.Parser.natMaybeZero : Lean.Parsec Nat

def Lean.Json.Parser.num : Lean.Parsec Lean.JsonNumber

partial def Lean.Json.Parser.arrayCore (anyCore : Lean.Parsec Lean.Json) (acc : Array Lean.Json) : Lean.Parsec (Array Lean.Json)

partial def Lean.Json.Parser.objectCore (anyCore : Lean.Parsec Lean.Json) : Lean.Parsec (Lean.RBNode String fun x => Lean.Json)

partial def Lean.Json.Parser.anyCore : Lean.Parsec Lean.Json

def Lean.Json.Parser.any : Lean.Parsec Lean.Json

def Lean.Json.parse (s : String) : Except String Lean.Json