diff --git a/library/data/string.lean b/library/data/string.lean
index 3a53ad6bc..49971a69d 100644
--- a/library/data/string.lean
+++ b/library/data/string.lean
@@ -13,3 +13,38 @@ inhabited.mk (char.mk ff ff ff ff ff ff ff ff)
 
 protected definition string.is_inhabited [instance] : inhabited string :=
 inhabited.mk string.empty
+
+open decidable
+
+definition decidable_eq_char [instance] : ∀ c₁ c₂ : char, decidable (c₁ = c₂) :=
+begin
+  intro c₁ c₂,
+  cases c₁ with a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈,
+  cases c₂ with b₁ b₂ b₃ b₄ b₅ b₆ b₇ b₈,
+  apply (@by_cases (a₁ = b₁)), intros,
+  apply (@by_cases (a₂ = b₂)), intros,
+  apply (@by_cases (a₃ = b₃)), intros,
+  apply (@by_cases (a₄ = b₄)), intros,
+  apply (@by_cases (a₅ = b₅)), intros,
+  apply (@by_cases (a₆ = b₆)), intros,
+  apply (@by_cases (a₇ = b₇)), intros,
+  apply (@by_cases (a₈ = b₈)), intros,
+  left, congruence, repeat assumption,
+  repeat (intro n; right; intro h; injection h; refine absurd _ n; assumption)
+end
+
+open string
+
+definition decidable_eq_string [instance] : ∀ s₁ s₂ : string, decidable (s₁ = s₂)
+| empty       empty       := by left; reflexivity
+| empty       (str c₂ r₂) := by right; contradiction
+| (str c₁ r₁) empty       := by right; contradiction
+| (str c₁ r₁) (str c₂ r₂) :=
+  match decidable_eq_char c₁ c₂ with
+  | inl e₁ :=
+    match decidable_eq_string r₁ r₂ with
+    | inl e₂ := by left; congruence; repeat assumption
+    | inr n₂ := by right; intro h; injection h; refine absurd _ n₂; assumption
+    end
+  | inr n₁ := by right; intro h; injection h; refine absurd _ n₁; assumption
+  end