Lean.Data.Json.FromToJson

One or more equations did not get rendered due to their size.
Lean.NameMap.fromJson? x✝ = throw (toString "expected a `NameMap`, got '" ++ toString x✝ ++ toString "'")

source

instance Lean.instFromJsonNameMap {α : Type} [FromJson α] :

FromJson (NameMap α)

Equations

Lean.instFromJsonNameMap = { fromJson? := Lean.NameMap.fromJson? }

source

def Lean.NameMap.toJson {α : Type} [ToJson α] (m : NameMap α) :

Json

Equations

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

source

instance Lean.instToJsonNameMap {α : Type} [ToJson α] :

ToJson (NameMap α)

Equations

Lean.instToJsonNameMap = { toJson := Lean.NameMap.toJson }

source

def Lean.bignumFromJson? (j : Json) :

Except String Nat

Note that USizes and UInt64s are stored as strings because JavaScript cannot represent 64-bit numbers.

Equations

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

source

def Lean.bignumToJson (n : Nat) :

Json

Equations

Lean.bignumToJson n = Lean.Json.str (toString n)

source

def USize.fromJson? (j : Lean.Json) :

Except String USize

Equations

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

source

instance Lean.instFromJsonUSize :

FromJson USize

Equations

Lean.instFromJsonUSize = { fromJson? := USize.fromJson? }

source

instance Lean.instToJsonUSize :

ToJson USize

Equations

Lean.instToJsonUSize = { toJson := fun (v : USize) => Lean.bignumToJson v.toNat }

source

def UInt64.fromJson? (j : Lean.Json) :

Except String UInt64

Equations

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

source

instance Lean.instFromJsonUInt64 :

FromJson UInt64

Equations

Lean.instFromJsonUInt64 = { fromJson? := UInt64.fromJson? }

source

instance Lean.instToJsonUInt64 :

ToJson UInt64

Equations

Lean.instToJsonUInt64 = { toJson := fun (v : UInt64) => Lean.bignumToJson v.toNat }

source

def Float.toJson (x : Float) :

Lean.Json

Equations

x.toJson = match Lean.JsonNumber.fromFloat? x with | Sum.inl e => Lean.Json.str e | Sum.inr n => Lean.Json.num n

source

instance Lean.instToJsonFloat :

ToJson Float

Equations

Lean.instToJsonFloat = { toJson := Float.toJson }

source

def Float.fromJson? :

Lean.Json → Except String Float

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

source

instance Lean.instFromJsonFloat :

FromJson Float

Equations

Lean.instFromJsonFloat = { fromJson? := Float.fromJson? }

source

def Lean.RBMap.toJson {α : Type} {cmp : String → String → Ordering} [ToJson α] (m : RBMap String α cmp) :

Json

Equations

m.toJson = Lean.Json.obj (Lean.RBNode.map (fun (x : String) => Lean.toJson) m.val)

source

instance Lean.instToJsonRBMapString {α : Type} {cmp : String → String → Ordering} [ToJson α] :

ToJson (RBMap String α cmp)

Equations

Lean.instToJsonRBMapString = { toJson := Lean.RBMap.toJson }

source

def Lean.RBMap.fromJson? {α : Type} {cmp : String → String → Ordering} [FromJson α] (j : Json) :

Except String (RBMap String α cmp)

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

source

instance Lean.instFromJsonRBMapString {α : Type} {cmp : String → String → Ordering} [FromJson α] :

FromJson (RBMap String α cmp)

Equations

Lean.instFromJsonRBMapString = { fromJson? := Lean.RBMap.fromJson? }

source

def Lean.Json.Structured.fromJson? :

Json → Except String Structured

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 "'")

source

instance Lean.Json.instFromJsonStructured :

FromJson Structured

Equations

Lean.Json.instFromJsonStructured = { fromJson? := Lean.Json.Structured.fromJson? }

source

def Lean.Json.Structured.toJson :

Structured → Json

Equations

(Lean.Json.Structured.arr a).toJson = Lean.Json.arr a
(Lean.Json.Structured.obj o).toJson = Lean.Json.obj o

source

instance Lean.Json.instToJsonStructured :

ToJson Structured

Equations

Lean.Json.instToJsonStructured = { toJson := Lean.Json.Structured.toJson }

source

def Lean.Json.toStructured? {α : Type u_1} [ToJson α] (v : α) :

Except String Structured

Equations

Lean.Json.toStructured? v = Lean.fromJson? (Lean.toJson v)

source

def Lean.Json.getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) :

Except String α

Equations

j.getObjValAs? α k = Lean.fromJson? (j.getObjValD k)

source

def Lean.Json.setObjValAs! (j : Json) {α : Type u} [ToJson α] (k : String) (v : α) :

Json

Equations

j.setObjValAs! k v = j.setObjVal! k (Lean.toJson v)

source

def Lean.Json.opt {α : Type u_1} [ToJson α] (k : String) :

Option α → List (String × Json)

Equations

Lean.Json.opt k none = []
Lean.Json.opt k (some a) = [(k, Lean.toJson a)]

source

def Lean.Json.parseTagged (json : Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Name)) :

Except String (Array Json)

Parses a JSON-encoded structure or inductive constructor. Used mostly by deriving FromJson.

Equations

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