From 7a5fcfae8b2ce7ee4be50f2d1a1cd8dcb186595b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2020 10:45:27 -0700
Subject: [PATCH] feat: add `[recursor]` attribute to `Iff.elim`

---
 src/Init/Core.lean             | 1 +
 tests/lean/run/induction1.lean | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 850a760114..b29f991284 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -760,6 +760,7 @@ def Or.symm := @Or.swap
 /- xor -/
 def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
 
+@[recursor 5]
 theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
 Iff.rec h₁ h₂
 
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index 19e841103f..d7d7c4e00e 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -76,3 +76,9 @@ begin
   | nil       => exact rfl
   | cons z zs => exact absurd rfl (h z zs)
 end
+
+theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
+begin
+  induction h₁ using Iff.elim with
+  | _ h _ => exact h h₂
+end