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

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

Instances For

source
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.

Instances For

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

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

Instances For

source
partial def Lean.Json.Parser.strCore (acc : String) :
Std.Internal.Parsec.String.Parser String
source
@[inline]
def Lean.Json.Parser.str :
Std.Internal.Parsec.String.Parser String
Equations

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

Instances For

source
partial def Lean.Json.Parser.natCore (acc : Nat) :
Std.Internal.Parsec.String.Parser Nat
source
partial def Lean.Json.Parser.natCoreNumDigits (acc digits : Nat) :
Std.Internal.Parsec.String.Parser (Nat × Nat)
source
@[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)

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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.

Instances For

source
@[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.

Instances For

source
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

Instances For

source
partial def Lean.Json.Parser.arrayCore (acc : Array Json) :
Std.Internal.Parsec.String.Parser (Array Json)
source
partial def Lean.Json.Parser.objectCore (kvs : Std.TreeMap.Raw String Json compare) :
Std.Internal.Parsec.String.Parser (Std.TreeMap.Raw String Json compare)
source
partial def Lean.Json.Parser.anyCore :
Std.Internal.Parsec.String.Parser Json
source
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

Instances For

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

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

Instances For