@[inline]

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

Equations

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

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

Equations

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

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

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

Equations

• Lean.Json.Parser.str = Lean.Json.Parser.strCore ""

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

Equations

• Lean.Json.Parser.lookahead p desc = do let c ← Lean.Parsec.peek! if p c then pure () else Lean.Parsec.fail ("expected " ++ desc)

@[inline]

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

Equations

• Lean.Json.Parser.natNonZero = do Lean.Json.Parser.lookahead (fun (c : Char) => '1' ≤ c ∧ c ≤ '9') "1-9" let __discr ← Lean.Json.Parser.natCore 0 0 match __discr with | (n, snd) => pure n

@[inline]

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

Equations

• Lean.Json.Parser.natNumDigits = do Lean.Json.Parser.lookahead (fun (c : Char) => '0' ≤ c ∧ c ≤ '9') "digit" Lean.Json.Parser.natCore 0 0

@[inline]

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

Equations

• Lean.Json.Parser.natMaybeZero = do let __discr ← Lean.Json.Parser.natNumDigits match __discr with | (n, snd) => pure n

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

Equations

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

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 : String) => Lean.Json)

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

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

Equations

• Lean.Json.Parser.any = do Lean.Parsec.ws let res ← Lean.Json.Parser.anyCore Lean.Parsec.eof pure res

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

Equations

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