Documentation

ImportGraph.Lean.Json

Extra ToJson and FromJson instances #

source
@[instance_reducible]
def ImportGraph.Lean.Json.instToJsonUInt32_importGraph :
Lean.ToJson UInt32
Instances For
    source
    @[instance_reducible]
    def ImportGraph.Lean.Json.instFromJsonUInt32_importGraph :
    Lean.FromJson UInt32
    Instances For
      source
      def ImportGraph.Lean.Json.instToJsonError_importGraph.toJson :
      IO.Error → Lean.Json
      Instances For
        source
        @[instance_reducible]
        instance ImportGraph.Lean.Json.instToJsonError_importGraph :
        Lean.ToJson IO.Error
        source
        def ImportGraph.Lean.Json.instFromJsonError_importGraph.fromJson :
        Lean.Json → Except String IO.Error
        Instances For
          source
          @[instance_reducible]
          instance ImportGraph.Lean.Json.instFromJsonError_importGraph :
          Lean.FromJson IO.Error
          source
          @[instance_reducible]
          instance ImportGraph.Lean.Json.instReprError_importGraph :
          Repr IO.Error
          source
          def ImportGraph.Lean.Json.instReprError_importGraph.repr :
          IO.Error → Nat → Std.Format
          Instances For