From da4f552a7acd0d3f16c129ca61431a47ae15c8e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Mon, 20 Feb 2017 11:12:53 -0500
Subject: [PATCH] feat(library/init/meta): add decidable_eq for binder_info

---
 library/init/meta/mk_dec_eq_instance.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/init/meta/mk_dec_eq_instance.lean b/library/init/meta/mk_dec_eq_instance.lean
index 202647df5c..d5f746d474 100644
--- a/library/init/meta/mk_dec_eq_instance.lean
+++ b/library/init/meta/mk_dec_eq_instance.lean
@@ -125,6 +125,9 @@ do env ← get_env,
            return () },
    mk_dec_eq_instance_core
 
+meta instance binder_info.has_decidable_eq : decidable_eq binder_info :=
+by mk_dec_eq_instance
+
 end tactic
 
 /- instances of types in dependent files -/