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).

Instances For
    source
    @[inline]
    def Lake.JsonObject.mk (val : Std.TreeMap.Raw String Lean.Json compare) :
    JsonObject
    Instances For
      source
      @[inline]
      def Lake.JsonObject.empty :
      JsonObject
      Instances For
        source
        @[inline]
        def Lake.JsonObject.toJson (obj : JsonObject) :
        Lean.Json
        Instances For
          source
          @[implicit_reducible]
          instance Lake.JsonObject.instCoeJson :
          Coe JsonObject Lean.Json
          source
          @[implicit_reducible]
          instance Lake.JsonObject.instToJson :
          Lean.ToJson JsonObject
          source
          @[inline]
          def Lake.JsonObject.fromJson? (json : Lean.Json) :
          Except String JsonObject
          Instances For
            source
            @[implicit_reducible]
            instance Lake.JsonObject.instFromJson :
            Lean.FromJson JsonObject
            source
            @[inline]
            def Lake.JsonObject.contains (obj : JsonObject) (prop : String) :
            Bool
            Instances For
              source
              def Lake.JsonObject.insertJson (obj : JsonObject) (prop : String) (val : Lean.Json) :
              JsonObject
              Instances For
                source
                @[inline]
                def Lake.JsonObject.insert {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val : α) :
                JsonObject
                Instances For
                  source
                  @[inline]
                  def Lake.JsonObject.insertSome {α : Type u_1} [Lean.ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) :
                  JsonObject
                  Instances For
                    source
                    def Lake.JsonObject.erase (obj : JsonObject) (prop : String) :
                    JsonObject
                    Instances For
                      source
                      def Lake.JsonObject.getJson? (obj : JsonObject) (prop : String) :
                      Option Lean.Json
                      Instances For
                        source
                        @[inline]
                        def Lake.JsonObject.get {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) :
                        Except String α
                        Instances For
                          source
                          @[inline]
                          def Lake.JsonObject.get? {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) :
                          Except String (Option α)
                          Instances For
                            source
                            @[macro_inline]
                            def Lake.JsonObject.getD {α : Type u_1} [Lean.FromJson α] (obj : JsonObject) (prop : String) (default : α) :
                            Except String α
                            Instances For