Documentation

Lake.Util.JsonObject

JSON Object #

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

@[reducible, inline]

A JSON object (Json.obj data).

Equations
Instances For
    @[inline]
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[inline]
        Equations
        Instances For
          @[inline]
          def Lake.JsonObject.insert {α : Type u_1} [Lean.ToJson α] (obj : Lake.JsonObject) (prop : String) (val : α) :
          Equations
          Instances For
            @[inline]
            def Lake.JsonObject.insertSome {α : Type u_1} [Lean.ToJson α] (obj : Lake.JsonObject) (prop : String) (val? : Option α) :
            Equations
            • obj.insertSome prop (some val) = obj.insert prop val
            • obj.insertSome prop val? = obj
            Instances For
              Equations
              Instances For
                @[inline]
                Equations
                Instances For
                  @[inline]
                  def Lake.JsonObject.get {α : Type u_1} [Lean.FromJson α] (obj : Lake.JsonObject) (prop : String) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[macro_inline]
                      def Lake.JsonObject.getD {α : Type u_1} [Lean.FromJson α] (obj : Lake.JsonObject) (prop : String) (default : α) :
                      Equations
                      • obj.getD prop default = do let __do_liftobj.get? prop pure (__do_lift.getD default)
                      Instances For