Equations
- Lean.instHashableJsonNumber = { hash := Lean.hashJsonNumber✝ }
Equations
- Lean.JsonNumber.fromNat n = { mantissa := ↑n, exponent := 0 }
Instances For
Equations
- Lean.JsonNumber.fromInt n = { mantissa := n, exponent := 0 }
Instances For
Equations
- Lean.JsonNumber.instCoeNat = { coe := Lean.JsonNumber.fromNat }
Equations
- Lean.JsonNumber.instCoeInt = { coe := Lean.JsonNumber.fromInt }
Equations
- Lean.JsonNumber.instOfNat = { ofNat := Lean.JsonNumber.fromNat n }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.JsonNumber.ltProp = { lt := fun (a b : Lean.JsonNumber) => a.lt b = true }
Instances For
Equations
- a.instDecidableLt b = inferInstanceAs (Decidable (a.lt b = true))
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 }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lean.JsonNumber.instToString = { toString := Lean.JsonNumber.toString }
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
- Lean.JsonNumber.instNeg = { neg := fun (jn : Lean.JsonNumber) => { mantissa := -jn.mantissa, exponent := jn.exponent } }
Equations
- Lean.JsonNumber.instInhabited = { default := 0 }
Equations
Instances For
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.
Instances For
Equations
- Lean.strLt a b = decide (a < b)
Instances For
Equations
- Lean.instInhabitedJson = { default := Lean.Json.null }
Equations
- Lean.Json.instBEq = { beq := Lean.Json.beq' }
Equations
- Lean.Json.instHashable = { hash := Lean.Json.hash' }
Equations
- Lean.Json.instCoeNat = { coe := fun (n : Nat) => Lean.Json.num (Lean.JsonNumber.fromNat n) }
Equations
- Lean.Json.instCoeInt = { coe := fun (n : Int) => Lean.Json.num (Lean.JsonNumber.fromInt n) }
Equations
- Lean.Json.instCoeString = { coe := Lean.Json.str }
Equations
- Lean.Json.instCoeBool = { coe := Lean.Json.bool }
Equations
- Lean.Json.instOfNat = { ofNat := Lean.Json.num (Lean.JsonNumber.fromNat n) }
Equations
- x.isNull = match x with | Lean.Json.null => true | x => false
Instances For
Equations
- x.getObj? = match x with | Lean.Json.obj kvs => pure kvs | x => throw "object expected"
Instances For
Equations
- x.getStr? = match x with | Lean.Json.str s => pure s | x => throw "String expected"
Instances For
Equations
- x.getInt? = match x with | Lean.Json.num { mantissa := i, exponent := 0 } => pure i | x => throw "Integer expected"
Instances For
Equations
- x.getBool? = match x with | Lean.Json.bool b => pure b | x => throw "Bool expected"
Instances For
Equations
- x.getNum? = match x with | Lean.Json.num n => pure n | x => throw "number expected"
Instances For
Equations
- j.getObjValD k = (j.getObjVal? k).toOption.getD Lean.Json.null
Instances For
Assuming both inputs o₁, o₂
are json objects, will compute {...o₁, ...o₂}
.
If o₁
is not a json object, o₂
will be returned.
Equations
- x✝.mergeObj 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₂
Instances For
- arr: Array Lean.Json → Lean.Json.Structured
- obj: (Lean.RBNode String fun (x : String) => Lean.Json) → Lean.Json.Structured
Instances For
Equations
instance
Lean.Json.instCoeRBNodeStringStructured :
Coe (Lean.RBNode String fun (x : String) => Lean.Json) Lean.Json.Structured