Equations
- Lean.instFromJsonJson = { fromJson? := Except.ok }
Equations
- Lean.instFromJsonJsonNumber = { fromJson? := Lean.Json.getNum? }
Equations
- Lean.instToJsonJsonNumber = { toJson := Lean.Json.num }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instToJsonEmpty = { toJson := fun (a : Empty) => nomatch a }
Equations
- Lean.instFromJsonBool = { fromJson? := Lean.Json.getBool? }
Equations
- Lean.instToJsonBool = { toJson := fun (b : Bool) => Lean.Json.bool b }
Equations
- Lean.instFromJsonNat = { fromJson? := Lean.Json.getNat? }
Equations
- Lean.instToJsonNat = { toJson := fun (n : Nat) => Lean.Json.num (Lean.JsonNumber.fromNat n) }
Equations
- Lean.instFromJsonInt = { fromJson? := Lean.Json.getInt? }
Equations
- Lean.instToJsonInt = { toJson := fun (n : Int) => Lean.Json.num (Lean.JsonNumber.fromInt n) }
Equations
- Lean.instFromJsonString = { fromJson? := Lean.Json.getStr? }
Equations
- Lean.instToJsonString = { toJson := fun (s : String) => Lean.Json.str s }
Equations
- Lean.instFromJsonFilePath = { fromJson? := fun (j : Lean.Json) => System.FilePath.mk <$> j.getStr? }
Equations
- Lean.instToJsonFilePath = { toJson := fun (p : System.FilePath) => Lean.Json.str p.toString }
Equations
- Array.fromJson? (Lean.Json.arr a) = Array.mapM Lean.fromJson? a
- Array.fromJson? x✝ = throw (toString "expected JSON array, got '" ++ toString x✝ ++ toString "'")
Instances For
Equations
- Lean.instFromJsonArray = { fromJson? := Array.fromJson? }
Equations
- a.toJson = Lean.Json.arr (Array.map Lean.toJson a)
Instances For
Equations
- Lean.instToJsonArray = { toJson := Array.toJson }
Equations
Instances For
Equations
- Lean.instFromJsonList = { fromJson? := List.fromJson? }
Equations
- a.toJson = Lean.toJson a.toArray
Instances For
Equations
- Lean.instToJsonList = { toJson := List.toJson }
Equations
Instances For
Equations
- Lean.instFromJsonOption = { fromJson? := Option.fromJson? }
Equations
- none.toJson = Lean.Json.null
- (some a).toJson = Lean.toJson a
Instances For
Equations
- Lean.instToJsonOption = { toJson := Option.toJson }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.instFromJsonProd = { fromJson? := Prod.fromJson? }
Equations
Instances For
Equations
- Lean.instToJsonProd = { toJson := Prod.toJson }
Equations
- Lean.instFromJsonName = { fromJson? := Lean.Name.fromJson? }
Equations
- Lean.instToJsonName = { toJson := fun (n : Lean.Name) => Lean.Json.str (toString n) }
Equations
- Lean.instFromJsonNameMap = { fromJson? := Lean.NameMap.fromJson? }
Equations
- Lean.instToJsonNameMap = { toJson := Lean.NameMap.toJson }
Equations
Instances For
Equations
- Lean.instFromJsonUSize = { fromJson? := USize.fromJson? }
Equations
- Lean.instToJsonUSize = { toJson := fun (v : USize) => Lean.bignumToJson v.toNat }
Equations
- Lean.instFromJsonUInt64 = { fromJson? := UInt64.fromJson? }
Equations
- Lean.instToJsonUInt64 = { toJson := fun (v : UInt64) => Lean.bignumToJson v.toNat }
Equations
- x.toJson = match Lean.JsonNumber.fromFloat? x with | Sum.inl e => Lean.Json.str e | Sum.inr n => Lean.Json.num n
Instances For
Equations
- Lean.instToJsonFloat = { toJson := Float.toJson }
Equations
- Float.fromJson? (Lean.Json.str "Infinity") = Except.ok (1.0 / 0.0)
- Float.fromJson? (Lean.Json.str "-Infinity") = Except.ok (-1.0 / 0.0)
- Float.fromJson? (Lean.Json.str "NaN") = Except.ok (0.0 / 0.0)
- Float.fromJson? (Lean.Json.num jn) = Except.ok jn.toFloat
- Float.fromJson? x✝ = Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."
Instances For
Equations
- Lean.instFromJsonFloat = { fromJson? := Float.fromJson? }
def
Lean.RBMap.toJson
{α : Type}
{cmp : String → String → Ordering}
[ToJson α]
(m : RBMap String α cmp)
:
Equations
- m.toJson = Lean.Json.obj (Lean.RBNode.map (fun (x : String) => Lean.toJson) m.val)
Instances For
Equations
- Lean.instToJsonRBMapString = { toJson := Lean.RBMap.toJson }
Equations
- Lean.RBMap.fromJson? j = do let o ← j.getObj? Lean.RBNode.foldM (fun (x : Lean.RBMap String α cmp) (k : String) (v : Lean.Json) => x.insert k <$> Lean.fromJson? v) ∅ o
Instances For
Equations
- Lean.instFromJsonRBMapString = { fromJson? := Lean.RBMap.fromJson? }
Equations
- Lean.Json.Structured.fromJson? (Lean.Json.arr a) = pure (Lean.Json.Structured.arr a)
- Lean.Json.Structured.fromJson? (Lean.Json.obj o) = pure (Lean.Json.Structured.obj o)
- Lean.Json.Structured.fromJson? x✝ = throw (toString "expected structured object, got '" ++ toString x✝ ++ toString "'")
Instances For
Equations
- Lean.Json.instFromJsonStructured = { fromJson? := Lean.Json.Structured.fromJson? }
Equations
Instances For
Equations
Equations
Instances For
Equations
- j.getObjValAs? α k = Lean.fromJson? (j.getObjValD k)
Instances For
Equations
- j.setObjValAs! k v = j.setObjVal! k (Lean.toJson v)