From d2e393c779ecdfa087f02574b74c95d39349ce56 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Jan 2017 16:02:17 -0800
Subject: [PATCH] feat(library/init/logic): allow exists.intro to be used in
 pattern matching

---
 library/init/logic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 31f14818b2..334aee2423 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -542,6 +542,7 @@ inductive Exists {α : Type u} (p : α → Prop) : Prop
 
 attribute [intro] Exists.intro
 
+@[pattern]
 def exists.intro := @Exists.intro
 
 notation `exists` binders `, ` r:(scoped P, Exists P) := r