Documentation

Lean.Data.Json.FromToJson

class Lean.FromJson (α : Type u) :
Instances
    class Lean.ToJson (α : Type u) :
    • toJson : αJson
    Instances
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      Equations
      Instances For
        def Array.toJson {α : Type u_1} [Lean.ToJson α] (a : Array α) :
        Equations
        Instances For
          instance Lean.instToJsonArray {α : Type u_1} [ToJson α] :
          Equations
          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
            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
              • One or more equations did not get rendered due to their size.
              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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For
                      def Lean.NameMap.toJson {α : Type} [ToJson α] (m : NameMap α) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  def Lean.RBMap.toJson {α : Type} {cmp : StringStringOrdering} [ToJson α] (m : RBMap String α cmp) :
                                  Equations
                                  Instances For
                                    def Lean.RBMap.fromJson? {α : Type} {cmp : StringStringOrdering} [FromJson α] (j : Json) :
                                    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
                                            • One or more equations did not get rendered due to their size.
                                            Instances For