From 73b4e424857989c18e2ccc434941e76df5edf06b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 May 2017 13:17:22 -0700
Subject: [PATCH] chore(frontends/lean,library): fix character pretty printer

---
 library/init/data/to_string.lean            |  2 +-
 src/library/string.cpp                      |  4 ++--
 tests/lean/char_lits.lean.expected.out      |  8 +++----
 tests/lean/curly_notation.lean.expected.out |  2 +-
 tests/lean/hex_char.lean.expected.out       |  6 ++---
 tests/lean/pp_char_bug.lean.expected.out    | 26 ++++++++++-----------
 6 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index 6310d3c2b4..7f4766e873 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -85,7 +85,7 @@ else if  char.to_nat c <= 31 then "\\x" ++ char_to_hex c
 else [c]
 
 instance : has_to_string char :=
-⟨λ c, "#\"" ++ char.quote_core c ++ "\""⟩
+⟨λ c, "'" ++ char.quote_core c ++ "'"⟩
 
 def string.quote_aux : string → string
 | []      := ""
diff --git a/src/library/string.cpp b/src/library/string.cpp
index 87db1c0514..7a89a6a614 100644
--- a/src/library/string.cpp
+++ b/src/library/string.cpp
@@ -49,9 +49,9 @@ static void display_char_literal_core(std::ostream & out, char c, bool in_string
 }
 
 static void display_char_literal(std::ostream & out, char c) {
-    out << "#\"";
+    out << "'";
     display_char_literal_core(out, c, false);
-    out << "\"";
+    out << "'";
 }
 
 static void display_string_literal(std::ostream & out, std::string const & s) {
diff --git a/tests/lean/char_lits.lean.expected.out b/tests/lean/char_lits.lean.expected.out
index ccf7bf9e8e..5949b9a59d 100644
--- a/tests/lean/char_lits.lean.expected.out
+++ b/tests/lean/char_lits.lean.expected.out
@@ -1,7 +1,7 @@
-#"a" : char
-#"a"
-#"\n"
-#"\\"
+'a' : char
+'a'
+'\n'
+'\\'
 aaa\
 
 
diff --git a/tests/lean/curly_notation.lean.expected.out b/tests/lean/curly_notation.lean.expected.out
index 4e2a858f19..816c0556a2 100644
--- a/tests/lean/curly_notation.lean.expected.out
+++ b/tests/lean/curly_notation.lean.expected.out
@@ -4,7 +4,7 @@
 def s1 : set ℕ :=
 {1, 2 + 3, 3, 4}
 def s2 : set char :=
-{#"a", #"b", #"c"}
+{'a', 'b', 'c'}
 def s3 : set string :=
 {"hello", "world"}
 {a ∈ s1 | a > 1} : set ℕ
diff --git a/tests/lean/hex_char.lean.expected.out b/tests/lean/hex_char.lean.expected.out
index 0fa2564414..a252a09df7 100644
--- a/tests/lean/hex_char.lean.expected.out
+++ b/tests/lean/hex_char.lean.expected.out
@@ -1,3 +1,3 @@
-#"A"
-#"B"
-#"C"
+'A'
+'B'
+'C'
diff --git a/tests/lean/pp_char_bug.lean.expected.out b/tests/lean/pp_char_bug.lean.expected.out
index fabfc42301..18c710de9e 100644
--- a/tests/lean/pp_char_bug.lean.expected.out
+++ b/tests/lean/pp_char_bug.lean.expected.out
@@ -1,15 +1,15 @@
 {val := 2, is_lt := of_as_true trivial} : fin 5
 {val := 1, is_lt := of_as_true trivial} : fin 3
-#"a" : char
-to_string #"a" : string
-"#\"a\""
-#"a"
-#"\x01"
-#"\x01"
-#"\x14"
-#"\x01" : char
-#"\x14" : char
-#"\x0f" : char
-#"\x10" : char
-#"\x0f"
-#"\x10"
+'a' : char
+to_string 'a' : string
+"'a'"
+'a'
+'\x01'
+'\x01'
+'\x14'
+'\x01' : char
+'\x14' : char
+'\x0f' : char
+'\x10' : char
+'\x0f'
+'\x10'