A RFC 8259 JSON parser.

structure Parser.Json.Number : Type

Can only be constructed by the number parser.

• raw : String

def Parser.Json.instReprNumber.repr : Number → ℕ → Std.Format

Equations

• Parser.Json.instReprNumber.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "raw" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.raw)).group) " }"

@[instance_reducible]

instance Parser.Json.instReprNumber : Repr Number

Equations

• Parser.Json.instReprNumber = { reprPrec := Parser.Json.instReprNumber.repr }

def Parser.Json.instBEqNumber.beq : Number → Number → Bool

Equations

• Parser.Json.instBEqNumber.beq { raw := a } { raw := b } = (a == b)
• Parser.Json.instBEqNumber.beq x✝¹ x✝ = false

@[instance_reducible]

instance Parser.Json.instBEqNumber : BEq Number

Equations

• Parser.Json.instBEqNumber = { beq := Parser.Json.instBEqNumber.beq }

inductive Parser.Json.Value : Type

• null : Value
• bool (value : Bool) : Value
• number (value : Number) : Value
• string (value : String) : Value
• array (values : List Value) : Value
• object (members : List (String × Value)) : Value

@[instance_reducible]

instance Parser.Json.instReprValue : Repr Value

Equations

• Parser.Json.instReprValue = { reprPrec := Parser.Json.instReprValue.repr }

partial def Parser.Json.instReprValue.repr : Value → ℕ → Std.Format

partial def Parser.Json.instBEqValue.beq : Value → Value → Bool

@[instance_reducible]

instance Parser.Json.instBEqValue : BEq Value

Equations

• Parser.Json.instBEqValue = { beq := Parser.Json.instBEqValue.beq }

def Parser.Json.number : Utf8Parser Error conditional Number

Equations

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

def Parser.Json.string : Utf8Parser Error conditional String

Equations

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

def Parser.Json.value : Utf8Parser Error conditional Value

Equations

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

def Parser.Json.json : Utf8Parser Error conditional Value

Parse a JSON document.

Equations

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