diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 7f22e69d0c..e3e3aaeed6 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -9,9 +9,6 @@ import logic tools.helper_tactics data.nat.order data.nat.sub
 open eq.ops nat prod function option
 
 namespace list
-notation h :: t  := cons h t
-notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
-
 variable {T : Type}
 
 lemma cons_ne_nil [simp] (a : T) (l : list T) : a::l ≠ [] :=
@@ -30,12 +27,6 @@ take l₁ l₂, assume Pe, tail_eq_of_cons_eq Pe
 
 /- append -/
 
-definition append : list T → list T → list T
-| []       l := l
-| (h :: s) t := h :: (append s t)
-
-notation l₁ ++ l₂ := append l₁ l₂
-
 theorem append_nil_left [simp] (t : list T) : [] ++ t = t :=
 rfl
 
@@ -49,10 +40,6 @@ theorem append.assoc [simp] : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
 sorry -- by rec_inst_simp
 
 /- length -/
-definition length : list T → nat
-| []       := 0
-| (a :: l) := length l + 1
-
 theorem length_nil [simp] : length (@nil T) = 0 :=
 rfl
 
diff --git a/library/init/char.lean b/library/init/char.lean
index 79fbc57a0b..847ec174fc 100644
--- a/library/init/char.lean
+++ b/library/init/char.lean
@@ -14,6 +14,8 @@ namespace char
 definition of_nat [coercion] (n : nat) : char :=
 if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial
 
+definition to_nat (c : char) : nat :=
+fin.val c
 end char
 
 definition char.has_decidable_eq [instance] : decidable_eq char :=
diff --git a/library/init/default.lean b/library/init/default.lean
index 610201ef5f..0b18777e88 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -8,4 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
-import init.monad init.fin init.list init.char init.string
+import init.monad init.fin init.list init.char init.string init.to_string
diff --git a/library/init/list.lean b/library/init/list.lean
index 398691ca50..5d401fe5df 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -24,3 +24,21 @@ list.rec_on l₁
            decidable.cases_on (ih l₂)
              (λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne)))
              (λ He  : l₁ = l₂, tt (congr (congr_arg cons Hab) He)))))
+
+namespace list
+notation h :: t  := cons h t
+notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
+
+variable {A : Type}
+
+definition append : list A → list A → list A
+| []       l := l
+| (h :: s) t := h :: (append s t)
+
+notation l₁ ++ l₂ := append l₁ l₂
+
+definition length : list A → nat
+| []       := 0
+| (a :: l) := length l + 1
+
+end list
diff --git a/library/init/string.lean b/library/init/string.lean
index aa2c2b6902..a8872901bf 100644
--- a/library/init/string.lean
+++ b/library/init/string.lean
@@ -4,11 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.char
+import init.char init.list
 
 definition string [reducible] := list char
 
 namespace string
 definition empty : string := list.nil
 definition str : char → string → string := list.cons
+
+definition concat (a b : string) : string :=
+list.append b a
 end string
+
+definition string.has_add [instance] : has_add string :=
+has_add.mk string.concat
diff --git a/library/init/to_string.lean b/library/init/to_string.lean
new file mode 100644
index 0000000000..a1da098860
--- /dev/null
+++ b/library/init/to_string.lean
@@ -0,0 +1,74 @@
+-- Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+prelude
+import init.string init.bool init.subtype
+open bool list option sum prod sigma subtype nat
+
+structure has_to_string [class] (A : Type) :=
+(to_string : A → string)
+
+definition to_string {A : Type} [has_to_string A] : A → string :=
+has_to_string.to_string
+
+definition bool.has_to_string [instance] : has_to_string bool :=
+has_to_string.mk (λ b, cond b "tt" "ff")
+
+definition list.to_string_aux {A : Type} [has_to_string A] : bool → list A → string
+| _  []      := ""
+| tt (x::xs) := to_string x + list.to_string_aux ff xs
+| ff (x::xs) := ", " + to_string x + list.to_string_aux ff xs
+
+definition list.to_string {A : Type} [has_to_string A] : list A → string
+| []      := "[]"
+| (x::xs) := "[" + list.to_string_aux tt (x::xs) + "]"
+
+definition list.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (list A) :=
+has_to_string.mk list.to_string
+
+definition unit.has_to_string [instance] : has_to_string unit :=
+has_to_string.mk (λ u, "star")
+
+definition option.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (option A) :=
+has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " + to_string a + ")" end)
+
+definition sum.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (sum A B) :=
+has_to_string.mk (λ s, match s with | inl a := "(inl " + to_string a + ")" | inr b := "(inr " + to_string b + ")" end)
+
+definition prod.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (prod A B) :=
+has_to_string.mk (λ p, "(" + to_string (pr1 p) + ", " + to_string (pr2 p) + ")")
+
+definition sigma.has_to_string [instance] {A : Type} {B : A → Type} [has_to_string A] [s : ∀ x, has_to_string (B x)]
+                                          : has_to_string (sigma B) :=
+has_to_string.mk (λ p, "⟨"  + to_string (pr1 p) + ", " + to_string (pr2 p) + "⟩")
+
+definition subtype.has_to_string [instance] {A : Type} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) :=
+has_to_string.mk (λ s, to_string (elt_of s))
+
+definition char.quote_core (c : char) : string :=
+if       char.to_nat c = 10 then "\\n"
+else if  char.to_nat c = 92 then "\\\\"
+else if  char.to_nat c = 34 then "\\\""
+else c::nil
+
+definition char.has_to_sting [instance] : has_to_string char :=
+has_to_string.mk (λ c, "'" + char.quote_core c + "'")
+
+definition string.quote_aux : string → string
+| []      := ""
+| (x::xs) := string.quote_aux xs + char.quote_core x
+
+definition string.quote : string → string
+| []      := "\"\""
+| (x::xs) := "\"" + string.quote_aux (x::xs) + "\""
+
+definition string.has_to_string [instance] : has_to_string string :=
+has_to_string.mk string.quote
+
+/- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/
+definition nat.to_string : nat → string
+| 0        := "zero"
+| (succ a) := "(succ " + nat.to_string a + ")"
+
+definition nat.has_to_string [instance] : has_to_string nat :=
+has_to_string.mk nat.to_string