Documentation

Lean.Data.Json.Parser

@[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) [inst : 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

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

@[inline]

def Lean.Json.Parser.natNumDigits:

Lean.Parsec (Nat × Nat)

Equations

Lean.Json.Parser.natNumDigits = do Lean.Json.Parser.lookahead (fun c => Char.ofNat 48 ≤ c ∧ c ≤ Char.ofNat 57) "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 (Std.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

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.