chore(frontends/lean,library): fix character pretty printer

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
 | []      := ""

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) {

tests/lean/char_lits.lean.expected.out

@@ -1,7 +1,7 @@
-#"a" : char
-#"a"
-#"\n"
-#"\\"
+'a' : char
+'a'
+'\n'
+'\\'
 aaa\
 
 

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 ℕ

tests/lean/hex_char.lean.expected.out

@@ -1,3 +1,3 @@
-#"A"
-#"B"
-#"C"
+'A'
+'B'
+'C'

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'