Extra ToJson and FromJson instances

@[instance_reducible]

def ImportGraph.Lean.Json.instToJsonUInt32_importGraph : Lean.ToJson UInt32

Equations

• ImportGraph.Lean.Json.instToJsonUInt32_importGraph = { toJson := fun (uint : UInt32) => Lean.Json.num (Lean.JsonNumber.fromNat uint.toNat) }

@[instance_reducible]

def ImportGraph.Lean.Json.instFromJsonUInt32_importGraph : Lean.FromJson UInt32

Equations

• ImportGraph.Lean.Json.instFromJsonUInt32_importGraph = { fromJson? := fun (uint : Lean.Json) => Except.map UInt32.ofNat (Lean.fromJson? uint) }

def ImportGraph.Lean.Json.instToJsonError_importGraph.toJson : IO.Error → Lean.Json

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Lean.Json.instToJsonError_importGraph.toJson (IO.Error.otherError a a_1) = Lean.Json.mkObj [("otherError", Lean.Json.mkObj [("osCode", Lean.toJson a), ("details", Lean.toJson a_1)])]
• ImportGraph.Lean.Json.instToJsonError_importGraph.toJson (IO.Error.timeExpired a a_1) = Lean.Json.mkObj [("timeExpired", Lean.Json.mkObj [("osCode", Lean.toJson a), ("details", Lean.toJson a_1)])]
• ImportGraph.Lean.Json.instToJsonError_importGraph.toJson IO.Error.unexpectedEof = Lean.toJson "unexpectedEof"
• ImportGraph.Lean.Json.instToJsonError_importGraph.toJson (IO.Error.userError a) = Lean.Json.mkObj [("userError", Lean.Json.mkObj [("msg", Lean.toJson a)])]

@[instance_reducible]

instance ImportGraph.Lean.Json.instToJsonError_importGraph : Lean.ToJson IO.Error

Equations

• ImportGraph.Lean.Json.instToJsonError_importGraph = { toJson := ImportGraph.Lean.Json.instToJsonError_importGraph.toJson }

def ImportGraph.Lean.Json.instFromJsonError_importGraph.fromJson : Lean.Json → Except String IO.Error

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lean.Json.instFromJsonError_importGraph : Lean.FromJson IO.Error

Equations

• ImportGraph.Lean.Json.instFromJsonError_importGraph = { fromJson? := ImportGraph.Lean.Json.instFromJsonError_importGraph.fromJson }

@[instance_reducible]

instance ImportGraph.Lean.Json.instReprError_importGraph : Repr IO.Error

Equations

• ImportGraph.Lean.Json.instReprError_importGraph = { reprPrec := ImportGraph.Lean.Json.instReprError_importGraph.repr }

def ImportGraph.Lean.Json.instReprError_importGraph.repr : IO.Error → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.