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) : Lake.JsonObject

Equations

• Lake.JsonObject.mk val = val

@[inline]

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

Equations

• obj.toJson = Lean.Json.obj obj

instance Lake.JsonObject.instToJson : Lean.ToJson Lake.JsonObject

Equations

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

@[inline]

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

Equations

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

instance Lake.JsonObject.instFromJson : Lean.FromJson Lake.JsonObject

Equations

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

@[inline]

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

Equations

• obj.erase prop = Lean.RBNode.erase compare prop obj

@[inline]

def Lake.JsonObject.getJson? (obj : Lake.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 : Lake.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 : Lake.JsonObject) (prop : String) : Except String (Option α)

Equations

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

@[inline]

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

Equations

• obj.getD prop default = (fun (x : Option α) => x.getD default) <$> obj.get? prop