From 198be2c8a72a91139300ad22738e38d38dd4bf35 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Fri, 20 Aug 2021 22:33:20 +0200
Subject: [PATCH] chore: no backticks in Name JSON

---
 src/Lean/Data/Json/FromToJson.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 3199d4af04..0bba89ba93 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -69,12 +69,12 @@ instance [ToJson α] [ToJson β] : ToJson (α × β) where
 instance : FromJson Name where
   fromJson? j := do
     let s ← j.getStr?
-    let some n ← Syntax.decodeNameLit s
+    let some n ← Syntax.decodeNameLit ("`" ++ s)
       | throw s!"expected a `Name`, got '{j}'"
     return n
 
 instance : ToJson Name where
-  toJson n := toString (repr n)
+  toJson n := toString n
 
 /- Note that `USize`s and `UInt64`s are stored as strings because JavaScript
 cannot represent 64-bit numbers. -/
@@ -83,7 +83,7 @@ def bignumFromJson? (j : Json) : Except String Nat := do
   let some v ← Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
     | throw s!"expected a string-encoded number, got '{j}'"
   return v
-  
+
 def bignumToJson (n : Nat) : Json :=
   toString n