From 1d245bcb82f67ed2d35ae1a9b31a943843abce35 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 25 Mar 2024 20:09:44 +1100
Subject: [PATCH] chore: revert ToJson/FromJson Sum (#3759) (#3760)

Sorry, this was ill-considered, it doesn't round trip faithfully.
---
 src/Lean/Data/Json/FromToJson.lean | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index e32fbd3220..1cfbe06ffa 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -76,20 +76,6 @@ instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α
 instance [ToJson α] [ToJson β] : ToJson (α × β) where
   toJson := fun (a, b) => Json.arr #[toJson a, toJson b]
 
-instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α ⊕ β) where
-  fromJson? j := do
-    match fromJson? j with
-    | .ok (a : α) => return Sum.inl a
-    | .error _ =>
-      match fromJson? j with
-      | .ok (b : β) => return Sum.inr b
-      | .error _ => throw s!"expected either left or right of a sum type, got '{j}'"
-
-instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
-  toJson x := match x with
-  | .inl a => toJson a
-  | .inr b => toJson b
-
 instance : FromJson Name where
   fromJson? j := do
     let s ← j.getStr?
@@ -107,7 +93,7 @@ instance : ToJson Name where
 cannot represent 64-bit numbers. -/
 def bignumFromJson? (j : Json) : Except String Nat := do
   let s ← j.getStr?
-  let some v := Syntax.decodeNatLitVal? s
+  let some v := Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
     | throw s!"expected a string-encoded number, got '{j}'"
   return v