JSON Object

Defines a convenient wrapper type for JSON object data that makes indexing fields more convenient.

@[reducible, inline]

abbrev Lake.JsonObject : Type

A JSON object (Json.obj data).

Equations

• Lake.JsonObject = Lean.RBNode String fun (x : String) => Lean.Json

@[inline]

def Lake.JsonObject.mk (val : Lean.RBNode String fun (x : String) => Lean.Json) : JsonObject

Equations

• Lake.JsonObject.mk val = val

@[inline]

def Lake.JsonObject.toJson (obj : JsonObject) : Lean.Json

Equations

• obj.toJson = Lean.Json.obj obj

instance Lake.JsonObject.instCoeJson : Coe JsonObject Lean.Json

Equations

• Lake.JsonObject.instCoeJson = { coe := Lean.Json.obj }

instance Lake.JsonObject.instToJson : Lean.ToJson JsonObject

Equations

• Lake.JsonObject.instToJson = { toJson := Lake.JsonObject.toJson }

@[inline]

def Lake.JsonObject.fromJson? (json : Lean.Json) : Except String JsonObject

Equations

• Lake.JsonObject.fromJson? json = json.getObj?

instance Lake.JsonObject.instFromJson : Lean.FromJson JsonObject

Equations

• Lake.JsonObject.instFromJson = { fromJson? := Lake.JsonObject.fromJson? }

@[inline]

def Lake.JsonObject.insert {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val : α) : JsonObject

Equations

• obj.insert prop val = Lean.RBNode.insert compare obj prop (Lean.toJson val)

@[inline]

def Lake.JsonObject.insertSome {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) : JsonObject

Equations

• obj.insertSome prop (some val) = obj.insert prop val
• obj.insertSome prop val? = obj

def Lake.JsonObject.erase (obj : JsonObject) (prop : String) : JsonObject

Equations

• obj.erase prop = inline (Lean.RBNode.erase compare prop obj)

@[inline]

def Lake.JsonObject.getJson? (obj : JsonObject) (prop : String) : Option Lean.Json

Equations

• obj.getJson? prop = Lean.RBNode.find compare obj prop

@[inline]

def Lake.JsonObject.get {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) : Except String α

Equations

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

@[inline]

def Lake.JsonObject.get? {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) : Except String (Option α)

Equations

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

@[macro_inline]

def Lake.JsonObject.getD {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) (default : α) : Except String α

Equations

• obj.getD prop default = do let __do_lift ← obj.get? prop pure (__do_lift.getD default)