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 = Std.TreeMap.Raw String Lean.Json compare

@[inline]

def Lake.JsonObject.mk (val : Std.TreeMap.Raw String Lean.Json compare) : JsonObject

Equations

• Lake.JsonObject.mk val = val

@[inline]

def Lake.JsonObject.empty : JsonObject

Equations

• Lake.JsonObject.empty = Std.TreeMap.Raw.empty

@[inline]

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

Equations

• obj.toJson = Lean.Json.obj obj

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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_reducible]

instance Lake.JsonObject.instFromJson : Lean.FromJson JsonObject

Equations

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

@[inline]

def Lake.JsonObject.contains (obj : JsonObject) (prop : String) : Bool

Equations

• obj.contains prop = Std.TreeMap.Raw.contains obj prop

def Lake.JsonObject.insertJson (obj : JsonObject) (prop : String) (val : Lean.Json) : JsonObject

Equations

• obj.insertJson prop val = Std.TreeMap.Raw.insert obj prop (Lean.toJson val)

@[inline]

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

Equations

• obj.insert prop val = obj.insertJson 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 = Std.TreeMap.Raw.erase obj prop

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

Equations

• obj.getJson? prop = Std.TreeMap.Raw.get? 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.getAs (α : Type u_1) [Lean.FromJson α] (obj : JsonObject) (prop : String) : Except String α

Equations

• Lake.JsonObject.getAs α obj prop = obj.get prop

@[inline]

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

Equations

• obj.get? prop = match obj.getJson? prop with | none => pure none | some val => Except.mapError (fun (x : String) => toString prop ++ toString ": " ++ toString x) (Lean.fromJson? val)

@[inline]

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

Equations

• Lake.JsonObject.getAs? α obj prop = obj.get? prop

@[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)