Compare commits

...

1 Commits

Author SHA1 Message Date
Scott Morrison
84b1a20dfc Revert "chore: ToJson/FromJson Sum (#3759)"
This reverts commit a943a79bd3.
2024-03-25 19:54:19 +11:00

View File

@@ -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