# Documentation

Lean.Data.Json.Basic

Instances For
Equations
• = { mantissa := , exponent := 0 }
Equations
• = { mantissa := n, exponent := 0 }
Equations
Equations
Equations
• Lean.JsonNumber.instOfNatJsonNumber = { ofNat := }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x, x with | { mantissa := m, exponent := e }, s => { mantissa := m * Int.ofNat (10 ^ (s - e)), exponent := e - s }
Equations
• = match x, x with | { mantissa := m, exponent := e }, s => { mantissa := m, exponent := e + s }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• = match x with | { mantissa := m, exponent := e } => (if m 0 then 1.0 else -1.0) *

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) :
Equations
inductive Lean.Json :
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
instance Lean.Json.instOfNatJson {n : Nat} :
Equations
• Lean.Json.instOfNatJson = { ofNat := }
Equations
• = match x with | Lean.Json.null => true | x => false
Equations
• = match x with | => pure kvs | x => throw "object expected"
Equations
• = match x with | => pure a | x => throw "array expected"
Equations
• = match x with | => pure s | x => throw "String expected"
Equations
Equations
Equations
• = match x with | => pure b | x => throw "Bool expected"
Equations
• = match x with | => pure n | x => throw "number expected"
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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

Equations
Instances For
Equations