From 6f0d8cb258ce2cf3ea6de1d7c077bb5f99b5f637 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Nov 2016 11:28:20 -0800 Subject: [PATCH] refactor(library/init/string): do not mark string as reducible --- library/debugger/util.lean | 6 +++--- library/init/instances.lean | 3 +++ library/init/string.lean | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/library/debugger/util.lean b/library/debugger/util.lean index 3d0d3d0047..6b5f0c5642 100644 --- a/library/debugger/util.lean +++ b/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 := diff --git a/library/init/instances.lean b/library/init/instances.lean index bad511b45a..f5226cf551 100644 --- a/library/init/instances.lean +++ b/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 diff --git a/library/init/string.lean b/library/init/string.lean index ad205a5614..037ea6e26a 100644 --- a/library/init/string.lean +++ b/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