structure Lean.JsonNumber : Type

A decimal number represented as mantissa * 10^-exponent.

• mantissa : Int
• exponent : Nat

@[instance_reducible]

instance Lean.instDecidableEqJsonNumber : DecidableEq JsonNumber

def Lean.instDecidableEqJsonNumber.decEq (x✝ x✝¹ : JsonNumber) : Decidable (x✝ = x✝¹)

def Lean.instHashableJsonNumber.hash : JsonNumber → UInt64

@[instance_reducible]

instance Lean.instHashableJsonNumber : Hashable JsonNumber

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

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

@[instance_reducible]

instance Lean.JsonNumber.instCoeNat : Coe Nat JsonNumber

@[instance_reducible]

instance Lean.JsonNumber.instCoeInt : Coe Int JsonNumber

@[instance_reducible]

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

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

Represents n = mantissa * 10^-exponent as (sign, mantissa', exponent'), where sign ∈ {-1,0,1} and n = sign * 0.mantissa' * 10^exponent'.

This is a normal form: if m1 * 10^-e1 = m2 * 10^-e2, then normalize ⟨m1, e1⟩ == normalize ⟨m2, e2⟩.

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

@[instance_reducible]

instance Lean.JsonNumber.ltProp : LT JsonNumber

@[instance_reducible]

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

@[instance_reducible]

instance Lean.JsonNumber.instOrd : Ord JsonNumber

def Lean.JsonNumber.toString : JsonNumber → String

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

shiftl n s shifts n by s places to the left, i.e., multiplies it by 10^s.

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

shiftr n s shifts n by s places to the right, i.e., divides it by 10^s.

@[instance_reducible]

instance Lean.JsonNumber.instToString : ToString JsonNumber

@[instance_reducible]

instance Lean.JsonNumber.instRepr : Repr JsonNumber

@[instance_reducible]

instance Lean.JsonNumber.instOfScientific : OfScientific JsonNumber

@[instance_reducible]

instance Lean.JsonNumber.instNeg : Neg JsonNumber

@[instance_reducible]

instance Lean.JsonNumber.instInhabited : Inhabited JsonNumber

def Lean.JsonNumber.toFloat : JsonNumber → Float

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

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

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

inductive Lean.Json : Type

A JSON value.

• null : Json
• bool (b : Bool) : Json
• num (n : JsonNumber) : Json
• str (s : String) : Json
• arr (elems : Array Json) : Json
• obj (kvPairs : Std.TreeMap.Raw String Json compare) : Json

@[instance_reducible]

instance Lean.instInhabitedJson : Inhabited Json

@[instance_reducible]

instance Lean.Json.instBEq : BEq Json

@[instance_reducible]

instance Lean.Json.instHashable : Hashable Json

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

@[instance_reducible]

instance Lean.Json.instCoeNat : Coe Nat Json

@[instance_reducible]

instance Lean.Json.instCoeInt : Coe Int Json

@[instance_reducible]

instance Lean.Json.instCoeString : Coe String Json

@[instance_reducible]

instance Lean.Json.instCoeBool : Coe Bool Json

@[instance_reducible]

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

def Lean.Json.isNull : Json → Bool

def Lean.Json.getObj? : Json → Except String (Std.TreeMap.Raw String Json compare)

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

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

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

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

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

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

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

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

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

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

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

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

inductive Lean.Json.Structured : Type

• arr (elems : Array Json) : Structured
• obj (kvPairs : Std.TreeMap.Raw String Json compare) : Structured

@[instance_reducible]

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

@[instance_reducible]

instance Lean.Json.instCoeRawStringStructured : Coe (Std.TreeMap.Raw String Json compare) Structured