Documentation

Lean.Data.Json.FromToJson

class Lean.FromJson (α : Type u) :
Instances
    class Lean.ToJson (α : Type u) :
    Instances
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      instance Lean.instToJsonArray {α : Type u_1} [Lean.ToJson α] :
      Equations
      Equations
      instance Lean.instToJsonList {α : Type u_1} [Lean.ToJson α] :
      Equations
      • Lean.instToJsonList = { toJson := fun (xs : List α) => Lean.toJson xs.toArray }
      Equations
      Equations
      instance Lean.instFromJsonProd {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] :
      Equations
      • One or more equations did not get rendered due to their size.
      instance Lean.instToJsonProd {α : Type u_1} {β : Type u_2} [Lean.ToJson α] [Lean.ToJson β] :
      Lean.ToJson (α × β)
      Equations
      Equations
      • One or more equations did not get rendered due to their size.

      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.
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Instances For
          def Lean.Json.setObjValAs! (j : Lean.Json) {α : Type u} [Lean.ToJson α] (k : String) (v : α) :
          Equations
          Instances For
            def Lean.Json.opt {α : Type u_1} [Lean.ToJson α] (k : String) :
            Equations
            Instances For
              def Lean.Json.parseTagged (json : Lean.Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Lake.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