refactor(library/init/string): do not mark string as reducible

library/debugger/util.lean

@@ -19,12 +19,12 @@ def split (s : string) : list string :=
 (split_core s [])^.reverse
 
 def to_qualified_name_core : string → string → name
-| []      r := if r = [] then name.anonymous else mk_simple_name r^.reverse
+| []      r := if r = "" then name.anonymous else mk_simple_name r^.reverse
 | (c::cs) r :=
   if is_space c then to_qualified_name_core cs r
   else if c = #"." then
-       if r = [] then to_qualified_name_core cs []
-       else           name.mk_string r^.reverse (to_qualified_name_core cs [])
+       if r = ""   then to_qualified_name_core cs []
+       else             name.mk_string r^.reverse (to_qualified_name_core cs [])
   else to_qualified_name_core cs (c::r)
 
 def to_qualified_name (s : string) : name :=

library/init/instances.lean

@@ -14,6 +14,9 @@ by mk_dec_eq_instance
 instance {α : Type u} [decidable_eq α] : decidable_eq (list α) :=
 by mk_dec_eq_instance
 
+instance : decidable_eq string :=
+list.decidable_eq
+
 instance : decidable_eq occurrences :=
 by mk_dec_eq_instance
 

library/init/string.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 prelude
 import init.char init.list
 
-@[reducible] def string := list char
+def string := list char
 
 namespace string
 @[pattern] def empty : string := list.nil