structure Lean.JsonNumber : Type

• mantissa : Int
• exponent : Nat

instance Lean.instDecidableEqJsonNumber : DecidableEq Lean.JsonNumber

Equations

• Lean.instDecidableEqJsonNumber = Lean.decEqJsonNumber✝

def Lean.JsonNumber.fromNat (n : Nat) : Lean.JsonNumber

Equations

• Lean.JsonNumber.fromNat n = { mantissa := Int.ofNat n, exponent := 0 }

def Lean.JsonNumber.fromInt (n : Int) : Lean.JsonNumber

Equations

• Lean.JsonNumber.fromInt n = { mantissa := n, exponent := 0 }

instance Lean.JsonNumber.instCoeNatJsonNumber : Coe Nat Lean.JsonNumber

Equations

• Lean.JsonNumber.instCoeNatJsonNumber = { coe := Lean.JsonNumber.fromNat }

instance Lean.JsonNumber.instCoeIntJsonNumber : Coe Int Lean.JsonNumber

Equations

• Lean.JsonNumber.instCoeIntJsonNumber = { coe := Lean.JsonNumber.fromInt }

instance Lean.JsonNumber.instOfNatJsonNumber {n : Nat} : OfNat Lean.JsonNumber n

Equations

• Lean.JsonNumber.instOfNatJsonNumber = { ofNat := Lean.JsonNumber.fromNat n }

def Lean.JsonNumber.normalize : Lean.JsonNumber → Int × Nat × Int

Equations

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

def Lean.JsonNumber.lt (a : Lean.JsonNumber) (b : Lean.JsonNumber) : Bool

Equations

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

def Lean.JsonNumber.ltProp : LT Lean.JsonNumber

Equations

• Lean.JsonNumber.ltProp = { lt := fun (a b : Lean.JsonNumber) => Lean.JsonNumber.lt a b = true }

instance Lean.JsonNumber.instLTJsonNumber : LT Lean.JsonNumber

Equations

• Lean.JsonNumber.instLTJsonNumber = Lean.JsonNumber.ltProp

instance Lean.JsonNumber.instDecidableLtJsonNumberInstLTJsonNumber (a : Lean.JsonNumber) (b : Lean.JsonNumber) : Decidable (a < b)

Equations

• Lean.JsonNumber.instDecidableLtJsonNumberInstLTJsonNumber a b = inferInstanceAs (Decidable (Lean.JsonNumber.lt a b = true))

instance Lean.JsonNumber.instOrdJsonNumber : Ord Lean.JsonNumber

Equations

• Lean.JsonNumber.instOrdJsonNumber = { compare := fun (x y : Lean.JsonNumber) => if x < y then Ordering.lt else if x > y then Ordering.gt else Ordering.eq }

def Lean.JsonNumber.toString : Lean.JsonNumber → String

Equations

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

def Lean.JsonNumber.shiftl : Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

• Lean.JsonNumber.shiftl x✝ x = match x✝, x with | { mantissa := m, exponent := e }, s => { mantissa := m * Int.ofNat (10 ^ (s - e)), exponent := e - s }

def Lean.JsonNumber.shiftr : Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

• Lean.JsonNumber.shiftr x✝ x = match x✝, x with | { mantissa := m, exponent := e }, s => { mantissa := m, exponent := e + s }

instance Lean.JsonNumber.instToStringJsonNumber : ToString Lean.JsonNumber

Equations

• Lean.JsonNumber.instToStringJsonNumber = { toString := Lean.JsonNumber.toString }

instance Lean.JsonNumber.instReprJsonNumber : Repr Lean.JsonNumber

Equations

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

instance Lean.JsonNumber.instOfScientificJsonNumber : OfScientific Lean.JsonNumber

Equations

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

instance Lean.JsonNumber.instNegJsonNumber : Neg Lean.JsonNumber

Equations

• Lean.JsonNumber.instNegJsonNumber = { neg := fun (jn : Lean.JsonNumber) => { mantissa := -jn.mantissa, exponent := jn.exponent } }

instance Lean.JsonNumber.instInhabitedJsonNumber : Inhabited Lean.JsonNumber

Equations

• Lean.JsonNumber.instInhabitedJsonNumber = { default := 0 }

def Lean.JsonNumber.toFloat : Lean.JsonNumber → Float

Equations

• Lean.JsonNumber.toFloat x = match x with | { mantissa := m, exponent := e } => (if m ≥ 0 then 1.0 else -1.0) * OfScientific.ofScientific (Int.natAbs m) true e

def Lean.JsonNumber.fromFloat? (x : Float) : String ⊕ Lean.JsonNumber

Attempts to convert a float to a JsonNumber, if the number isn't finite returns the appropriate string from "NaN", "Infinity", "-Infinity".

Equations

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

def Lean.strLt (a : String) (b : String) : Bool

Equations

• Lean.strLt a b = decide (a < b)

inductive Lean.Json : Type

• null: Lean.Json
• bool: Bool → Lean.Json
• num: Lean.JsonNumber → Lean.Json
• str: String → Lean.Json
• arr: Array Lean.Json → Lean.Json
• obj: (Lean.RBNode String fun (x : String) => Lean.Json) → Lean.Json

instance Lean.instInhabitedJson : Inhabited Lean.Json

Equations

• Lean.instInhabitedJson = { default := Lean.Json.null }

instance Lean.Json.instBEqJson : BEq Lean.Json

Equations

• Lean.Json.instBEqJson = { beq := Lean.Json.beq' }

def Lean.Json.mkObj (o : List (String × Lean.Json)) : Lean.Json

Equations

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

instance Lean.Json.instCoeNatJson : Coe Nat Lean.Json

Equations

• Lean.Json.instCoeNatJson = { coe := fun (n : Nat) => Lean.Json.num (Lean.JsonNumber.fromNat n) }

instance Lean.Json.instCoeIntJson : Coe Int Lean.Json

Equations

• Lean.Json.instCoeIntJson = { coe := fun (n : Int) => Lean.Json.num (Lean.JsonNumber.fromInt n) }

instance Lean.Json.instCoeStringJson : Coe String Lean.Json

Equations

• Lean.Json.instCoeStringJson = { coe := Lean.Json.str }

instance Lean.Json.instCoeBoolJson : Coe Bool Lean.Json

Equations

• Lean.Json.instCoeBoolJson = { coe := Lean.Json.bool }

instance Lean.Json.instOfNatJson {n : Nat} : OfNat Lean.Json n

Equations

• Lean.Json.instOfNatJson = { ofNat := Lean.Json.num (Lean.JsonNumber.fromNat n) }

def Lean.Json.isNull : Lean.Json → Bool

Equations

• Lean.Json.isNull x = match x with | Lean.Json.null => true | x => false

def Lean.Json.getObj? : Lean.Json → Except String (Lean.RBNode String fun (x : String) => Lean.Json)

Equations

• Lean.Json.getObj? x = match x with | Lean.Json.obj kvs => pure kvs | x => throw "object expected"

def Lean.Json.getArr? : Lean.Json → Except String (Array Lean.Json)

Equations

• Lean.Json.getArr? x = match x with | Lean.Json.arr a => pure a | x => throw "array expected"

def Lean.Json.getStr? : Lean.Json → Except String String

Equations

• Lean.Json.getStr? x = match x with | Lean.Json.str s => pure s | x => throw "String expected"

def Lean.Json.getNat? : Lean.Json → Except String Nat

Equations

• Lean.Json.getNat? x = match x with | Lean.Json.num { mantissa := Int.ofNat n, exponent := 0 } => pure n | x => throw "Natural number expected"

def Lean.Json.getInt? : Lean.Json → Except String Int

Equations

• Lean.Json.getInt? x = match x with | Lean.Json.num { mantissa := i, exponent := 0 } => pure i | x => throw "Integer expected"

def Lean.Json.getBool? : Lean.Json → Except String Bool

Equations

• Lean.Json.getBool? x = match x with | Lean.Json.bool b => pure b | x => throw "Bool expected"

def Lean.Json.getNum? : Lean.Json → Except String Lean.JsonNumber

Equations

• Lean.Json.getNum? x = match x with | Lean.Json.num n => pure n | x => throw "number expected"

def Lean.Json.getObjVal? : Lean.Json → String → Except String Lean.Json

Equations

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

def Lean.Json.getArrVal? : Lean.Json → Nat → Except String Lean.Json

Equations

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

def Lean.Json.getObjValD (j : Lean.Json) (k : String) : Lean.Json

Equations

• Lean.Json.getObjValD j k = Option.getD (Except.toOption (Lean.Json.getObjVal? j k)) Lean.Json.null

def Lean.Json.setObjVal! : Lean.Json → String → Lean.Json → Lean.Json

Equations

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

def Lean.Json.mergeObj : Lean.Json → Lean.Json → Lean.Json

Assuming both inputs o₁, o₂ are json objects, will compute {...o₁, ...o₂}. If o₁ is not a json object, o₂ will be returned.

Equations

• Lean.Json.mergeObj x✝ x = match x✝, x with | Lean.Json.obj kvs₁, Lean.Json.obj kvs₂ => Lean.Json.obj (Lean.RBNode.fold (Lean.RBNode.insert compare) kvs₁ kvs₂) | x, j₂ => j₂

inductive Lean.Json.Structured : Type

• arr: Array Lean.Json → Lean.Json.Structured
• obj: (Lean.RBNode String fun (x : String) => Lean.Json) → Lean.Json.Structured

instance Lean.Json.instCoeArrayJsonStructured : Coe (Array Lean.Json) Lean.Json.Structured

Equations

• Lean.Json.instCoeArrayJsonStructured = { coe := Lean.Json.Structured.arr }

instance Lean.Json.instCoeRBNodeStringJsonStructured : Coe (Lean.RBNode String fun (x : String) => Lean.Json) Lean.Json.Structured

Equations

• Lean.Json.instCoeRBNodeStringJsonStructured = { coe := Lean.Json.Structured.obj }