structure Lean.JsonNumber : Type

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

• mantissa : Int
• exponent : Nat

@[instance_reducible]

instance Lean.instDecidableEqJsonNumber : DecidableEq JsonNumber

Equations

• Lean.instDecidableEqJsonNumber = Lean.instDecidableEqJsonNumber.decEq

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

Equations

• Lean.instDecidableEqJsonNumber.decEq { mantissa := a, exponent := a_1 } { mantissa := b, exponent := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Lean.instHashableJsonNumber.hash : JsonNumber → UInt64

Equations

• Lean.instHashableJsonNumber.hash { mantissa := a, exponent := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance Lean.instHashableJsonNumber : Hashable JsonNumber

Equations

• Lean.instHashableJsonNumber = { hash := Lean.instHashableJsonNumber.hash }

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instCoeNat : Coe Nat JsonNumber

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instCoeInt : Coe Int JsonNumber

Equations

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

@[instance_reducible]

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

Equations

• Lean.JsonNumber.instOfNat = { ofNat := Lean.JsonNumber.fromNat 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⟩.

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.ltProp : LT JsonNumber

Equations

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

@[instance_reducible]

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

Equations

• a.instDecidableLt b = instDecidableEqBool (a.lt b) true

@[instance_reducible]

instance Lean.JsonNumber.instOrd : Ord JsonNumber

Equations

• Lean.JsonNumber.instOrd = { 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 : JsonNumber → String

Equations

• One or more equations did not get rendered due to their size.
• { mantissa := m, exponent := 0 }.toString = m.repr

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.

Equations

• { mantissa := m, exponent := e }.shiftl x✝ = { mantissa := m * ↑(10 ^ (x✝ - e)), exponent := e - x✝ }

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.

Equations

• { mantissa := m, exponent := e }.shiftr x✝ = { mantissa := m, exponent := e + x✝ }

@[instance_reducible]

instance Lean.JsonNumber.instToString : ToString JsonNumber

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instRepr : Repr JsonNumber

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instOfScientific : OfScientific JsonNumber

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instNeg : Neg JsonNumber

Equations

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

@[instance_reducible]

instance Lean.JsonNumber.instInhabited : Inhabited JsonNumber

Equations

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

def Lean.JsonNumber.toFloat : JsonNumber → Float

Equations

• { mantissa := a, exponent := a_1 }.toFloat = (if a ≥ 0 then 1.0 else -1.0) * OfScientific.ofScientific a.natAbs true a_1

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".

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.Json.instBEq : BEq Json

Equations

• Lean.Json.instBEq = { beq := Lean.Json.instBEq._private_1 }

@[instance_reducible]

instance Lean.Json.instHashable : Hashable Json

Equations

• Lean.Json.instHashable = { hash := Lean.Json.instHashable._private_1 }

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

Equations

• Lean.Json.mkObj o = Lean.Json.obj (Std.TreeMap.Raw.ofList o compare)

@[instance_reducible]

instance Lean.Json.instCoeNat : Coe Nat Json

Equations

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

@[instance_reducible]

instance Lean.Json.instCoeInt : Coe Int Json

Equations

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

@[instance_reducible]

instance Lean.Json.instCoeString : Coe String Json

Equations

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

@[instance_reducible]

instance Lean.Json.instCoeBool : Coe Bool Json

Equations

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

@[instance_reducible]

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

Equations

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

def Lean.Json.isNull : Json → Bool

Equations

• Lean.Json.null.isNull = true
• x✝.isNull = false

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

Equations

• (Lean.Json.obj kvs).getObj? = pure kvs
• x✝.getObj? = throw "object expected"

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

Equations

• (Lean.Json.arr a).getArr? = pure a
• x✝.getArr? = throw "array expected"

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

Equations

• (Lean.Json.str s).getStr? = pure s
• x✝.getStr? = throw "String expected"

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

Equations

• (Lean.Json.num { mantissa := Int.ofNat n, exponent := 0 }).getNat? = pure n
• x✝.getNat? = throw "Natural number expected"

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

Equations

• (Lean.Json.num { mantissa := i, exponent := 0 }).getInt? = pure i
• x✝.getInt? = throw "Integer expected"

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

Equations

• (Lean.Json.bool b).getBool? = pure b
• x✝.getBool? = throw "Bool expected"

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

Equations

• (Lean.Json.num n).getNum? = pure n
• x✝.getNum? = throw "number expected"

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

Equations

• (Lean.Json.obj kvs).getObjVal? x✝ = match kvs.get? x✝ with | some v => pure v | none => throw (toString "property not found: " ++ toString x✝)
• x✝¹.getObjVal? x✝ = throw "object expected"

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

Equations

• (Lean.Json.arr a).getArrVal? x✝ = match a[x✝]? with | some v => pure v | none => throw (toString "index out of bounds: " ++ toString x✝)
• x✝¹.getArrVal? x✝ = throw "array expected"

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

Equations

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

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

Equations

• (Lean.Json.obj kvs).setObjVal! x✝¹ x✝ = Lean.Json.obj (kvs.insert x✝¹ x✝)
• x✝².setObjVal! x✝¹ x✝ = panicWithPosWithDecl "Lean.Data.Json.Basic" "Lean.Json.setObjVal!" 290 21 "Json.setObjVal!: not an object: {j}"

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.

Equations

• (Lean.Json.obj kvs₁).mergeObj (Lean.Json.obj kvs₂) = Lean.Json.obj (Std.TreeMap.Raw.foldl Std.TreeMap.Raw.insert kvs₁ kvs₂)
• x✝¹.mergeObj x✝ = x✝

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

Equations

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

@[instance_reducible]

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

Equations

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