Documentation

Lake.Util.JsonObject

JSON Object #

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

@[inline]
Equations
@[inline]
Equations
@[inline]
def Lake.JsonObject.insert {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val : α) :
Equations
@[inline]
def Lake.JsonObject.insertSome {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) :
Equations
  • obj.insertSome prop (some val) = obj.insert prop val
  • obj.insertSome prop val? = obj
Equations
@[inline]
Equations
@[inline]
def Lake.JsonObject.get {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : 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) :
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 : α) :
Equations
  • obj.getD prop default = do let __do_liftobj.get? prop pure (__do_lift.getD default)