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

@[inline]

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

Equations

• obj.toJson = Lean.Json.obj obj

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

Equations

• Lake.JsonObject.instCoeJson = { coe := Lean.Json.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

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

@[inline]

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

@[inline]

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[macro_inline]

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

Equations

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