Documentation

Lake.Util.JsonObject

JSON Object #

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

source
@[reducible, inline]
abbrev Lake.JsonObject :
Type

A JSON object (Json.obj data).

Equations
    Instances For
      source
      @[inline]
      def Lake.JsonObject.mk (val : Lean.RBNode String fun (x : String) => Lean.Json) :
      JsonObject
      Equations
        Instances For
          source
          @[inline]
          def Lake.JsonObject.toJson (obj : JsonObject) :
          Lean.Json
          Equations
            Instances For
              source
              instance Lake.JsonObject.instCoeJson :
              Coe JsonObject Lean.Json
              Equations
                source
                instance Lake.JsonObject.instToJson :
                Lean.ToJson JsonObject
                Equations
                  source
                  @[inline]
                  def Lake.JsonObject.fromJson? (json : Lean.Json) :
                  Except String JsonObject
                  Equations
                    Instances For
                      source
                      instance Lake.JsonObject.instFromJson :
                      Lean.FromJson JsonObject
                      Equations
                        source
                        @[inline]
                        def Lake.JsonObject.insert {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val : α) :
                        JsonObject
                        Equations
                          Instances For
                            source
                            @[inline]
                            def Lake.JsonObject.insertSome {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) :
                            JsonObject
                            Equations
                              Instances For
                                source
                                def Lake.JsonObject.erase (obj : JsonObject) (prop : String) :
                                JsonObject
                                Equations
                                  Instances For
                                    source
                                    @[inline]
                                    def Lake.JsonObject.getJson? (obj : JsonObject) (prop : String) :
                                    Option Lean.Json
                                    Equations
                                      Instances For
                                        source
                                        @[inline]
                                        def Lake.JsonObject.get {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) :
                                        Except String α
                                        Equations
                                          Instances For
                                            source
                                            @[inline]
                                            def Lake.JsonObject.get? {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) :
                                            Except String (Option α)
                                            Equations
                                              Instances For
                                                source
                                                @[macro_inline]
                                                def Lake.JsonObject.getD {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) (default : α) :
                                                Except String α
                                                Equations
                                                  Instances For