def Lean.Json.Parser.hexChar : Std.Internal.Parsec.String.Parser UInt16

Equations

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

def Lean.Json.Parser.finishSurrogatePair (low : UInt16) : Std.Internal.Parsec.String.Parser Char

Equations

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

def Lean.Json.Parser.escapedChar : Std.Internal.Parsec.String.Parser Char

Equations

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

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

@[inline]

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

Equations

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

partial def Lean.Json.Parser.natCore (acc : Nat) : Std.Internal.Parsec.String.Parser Nat

partial def Lean.Json.Parser.natCoreNumDigits (acc digits : Nat) : Std.Internal.Parsec.String.Parser (Nat × Nat)

@[inline]

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

Equations

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

@[inline]

def Lean.Json.Parser.natNonZero : Std.Internal.Parsec.String.Parser Nat

Equations

• Lean.Json.Parser.natNonZero = do Lean.Json.Parser.lookahead (fun (c : Char) => (decide ('1' ≤ c) && decide (c ≤ '9')) = true) "1-9" Lean.Json.Parser.natCore 0

@[inline]

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

Equations

• Lean.Json.Parser.natNumDigits = do Lean.Json.Parser.lookahead (fun (c : Char) => (decide ('0' ≤ c) && decide (c ≤ '9')) = true) "digit" Lean.Json.Parser.natCoreNumDigits 0 0

@[inline]

def Lean.Json.Parser.natMaybeZero : Std.Internal.Parsec.String.Parser Nat

Equations

• Lean.Json.Parser.natMaybeZero = do Lean.Json.Parser.lookahead (fun (c : Char) => (decide ('0' ≤ c) && decide (c ≤ '9')) = true) "0-9" Lean.Json.Parser.natCore 0

@[inline]

def Lean.Json.Parser.numSign : Std.Internal.Parsec.String.Parser Int

Equations

• Lean.Json.Parser.numSign = do let c ← Std.Internal.Parsec.peek! if (c == '-') = true then do Std.Internal.Parsec.skip pure (-1) else pure 1

@[inline]

def Lean.Json.Parser.nat : Std.Internal.Parsec.String.Parser Nat

Equations

• Lean.Json.Parser.nat = do let c ← Std.Internal.Parsec.peek! if (c == '0') = true then do Std.Internal.Parsec.skip pure 0 else Lean.Json.Parser.natNonZero

@[inline]

def Lean.Json.Parser.numWithDecimals : Std.Internal.Parsec.String.Parser JsonNumber

Equations

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

@[inline]

def Lean.Json.Parser.exponent (value : JsonNumber) : Std.Internal.Parsec.String.Parser JsonNumber

Equations

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

def Lean.Json.Parser.num : Std.Internal.Parsec.String.Parser JsonNumber

Equations

• Lean.Json.Parser.num = do let res ← Lean.Json.Parser.numWithDecimals Lean.Json.Parser.exponent res

partial def Lean.Json.Parser.arrayCore (acc : Array Json) : Std.Internal.Parsec.String.Parser (Array Json)

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

partial def Lean.Json.Parser.anyCore : Std.Internal.Parsec.String.Parser Json

def Lean.Json.Parser.any : Std.Internal.Parsec.String.Parser Json

Equations

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

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

Equations

• Lean.Json.parse s = Lean.Json.Parser.any.run s