Documentation

Lean.Data.Json.FromToJson

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

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

                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For
                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              def Lean.RBMap.toJson {α : Type} {cmp : StringStringOrdering} [ToJson α] (m : RBMap String α cmp) :
                                                                                              Equations
                                                                                                Instances For
                                                                                                  instance Lean.instToJsonRBMapString {α : Type} {cmp : StringStringOrdering} [ToJson α] :
                                                                                                  Equations
                                                                                                    def Lean.RBMap.fromJson? {α : Type} {cmp : StringStringOrdering} [FromJson α] (j : Json) :
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        instance Lean.instFromJsonRBMapString {α : Type} {cmp : StringStringOrdering} [FromJson α] :
                                                                                                        Equations
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  def Lean.Json.getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) :
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      def Lean.Json.setObjValAs! (j : Json) {α : Type u} [ToJson α] (k : String) (v : α) :
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          def Lean.Json.opt {α : Type u_1} [ToJson α] (k : String) :
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              def Lean.Json.parseTagged (json : Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Name)) :

                                                                                                                              Parses a JSON-encoded structure or inductive constructor. Used mostly by deriving FromJson.

                                                                                                                              Equations
                                                                                                                                Instances For