Documentation

Lean.Data.Json.FromToJson.Basic

class Lean.FromJson (α : Type u) :
Instances
    class Lean.ToJson (α : Type u) :
    • toJson : αJson
    Instances
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      @[implicit_reducible]
      Instances For
        @[implicit_reducible]
        instance Lean.instFromJsonArray {α : Type u_1} [FromJson α] :
        def Array.toJson {α : Type u_1} [Lean.ToJson α] (a : Array α) :
        Instances For
          @[implicit_reducible]
          instance Lean.instToJsonArray {α : Type u_1} [ToJson α] :
          def List.fromJson? {α : Type u_1} [Lean.FromJson α] (j : Lean.Json) :
          Instances For
            @[implicit_reducible]
            instance Lean.instFromJsonList {α : Type u_1} [FromJson α] :
            def List.toJson {α : Type u_1} [Lean.ToJson α] (a : List α) :
            Instances For
              @[implicit_reducible]
              instance Lean.instToJsonList {α : Type u_1} [ToJson α] :
              Instances For
                @[implicit_reducible]
                instance Lean.instFromJsonOption {α : Type u_1} [FromJson α] :
                def Option.toJson {α : Type u_1} [Lean.ToJson α] :
                Instances For
                  @[implicit_reducible]
                  instance Lean.instToJsonOption {α : Type u_1} [ToJson α] :
                  def Prod.fromJson? {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] :
                  Instances For
                    @[implicit_reducible]
                    instance Lean.instFromJsonProd {α : Type u} {β : Type v} [FromJson α] [FromJson β] :
                    FromJson (α × β)
                    def Prod.toJson {α : Type u_1} {β : Type u_2} [Lean.ToJson α] [Lean.ToJson β] :
                    α × βLean.Json
                    Instances For
                      @[implicit_reducible]
                      instance Lean.instToJsonProd {α : Type u_1} {β : Type u_2} [ToJson α] [ToJson β] :
                      ToJson (α × β)
                      @[implicit_reducible]
                      @[implicit_reducible]
                      Instances For
                        @[implicit_reducible]
                        def Lean.NameMap.toJson {α : Type} [ToJson α] (m : NameMap α) :
                        Instances For
                          @[implicit_reducible]
                          instance Lean.instToJsonNameMap {α : Type} [ToJson α] :

                          Note that USizes and UInt64s are stored as strings because JavaScript cannot represent 64-bit numbers.

                          Instances For
                            Instances For
                              @[implicit_reducible]
                              @[implicit_reducible]
                              @[implicit_reducible]
                              @[implicit_reducible]
                              Instances For
                                @[implicit_reducible]
                                @[implicit_reducible]
                                Instances For
                                  def Lean.Json.getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) :
                                  Instances For
                                    def Lean.Json.setObjValAs! (j : Json) {α : Type u} [ToJson α] (k : String) (v : α) :
                                    Instances For
                                      def Lean.Json.opt {α : Type u_1} [ToJson α] (k : String) :
                                      Instances For

                                        Returns the string value or single key name, if any.

                                        Instances For
                                          def Lean.Json.parseTagged (json : Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Name)) :
                                          Instances For
                                            def Lean.Json.parseCtorFields (json : Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Name)) :

                                            Parses a JSON-encoded structure or inductive constructor, assuming the tag has already been checked and nFields is nonzero. Used mostly by deriving FromJson.

                                            Instances For