From 780d3136868a3f50239f319d58e5ea92ff9d139b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Jun 2015 11:27:46 -0700
Subject: [PATCH] fix(library/annotation): add missing == and hash methods for
 annotation class

We have multiple annotations. The default == and hash methods were
ignoring that.
---
 src/library/annotation.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp
index c5763f948..242848eca 100644
--- a/src/library/annotation.cpp
+++ b/src/library/annotation.cpp
@@ -45,6 +45,16 @@ public:
         s.write_string(get_annotation_opcode());
         s << m_name;
     }
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto other_ptr = dynamic_cast<annotation_macro_definition_cell const *>(&other)) {
+            return m_name == other_ptr->m_name;
+        } else {
+            return false;
+        }
+    }
+    virtual unsigned hash() const {
+        return ::lean::hash(m_name.hash(), g_annotation->hash());
+    }
 };
 
 typedef std::unordered_map<name, macro_definition, name_hash, name_eq> annotation_macros;