From cb74ef1670ae75a1ffbc06ed358419dfca9873e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Dec 2017 16:21:49 -0800
Subject: [PATCH] chore(library/init/meta/interactive): fix docstring

---
 library/init/meta/interactive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 4ec4c0fb2b..3a94c14407 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -420,7 +420,7 @@ example (n : ℕ) : n = n :=
 begin
   with_cases { induction n },
   case nat.zero { reflexivity },
-  case nat.succ n' ih { reflexivity }
+  case nat.succ : n' ih { reflexivity }
 end
 ```