From f6e18045f34197280ab348577327a36613c18dfa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Jul 2013 15:59:10 -0700
Subject: [PATCH] Add eqp (pointer equality) tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/sexpr/sexpr.cpp       | 2 ++
 src/tests/sexpr/sexpr.cpp | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/src/sexpr/sexpr.cpp b/src/sexpr/sexpr.cpp
index 7a0cc7ce8..aa09d5804 100644
--- a/src/sexpr/sexpr.cpp
+++ b/src/sexpr/sexpr.cpp
@@ -168,6 +168,8 @@ unsigned length(sexpr const & s) {
 }
 
 bool operator==(sexpr const & a, sexpr const & b) {
+    if (eqp(a, b))
+        return true;
     sexpr::kind ka = a.get_kind();
     sexpr::kind kb = b.get_kind();
     if (ka != kb)
diff --git a/src/tests/sexpr/sexpr.cpp b/src/tests/sexpr/sexpr.cpp
index 43a5e4047..7d2bb96df 100644
--- a/src/tests/sexpr/sexpr.cpp
+++ b/src/tests/sexpr/sexpr.cpp
@@ -69,6 +69,10 @@ static void tst1() {
     lean_assert(append(nil(), l) == l);
     lean_assert(contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < 0; }));
     lean_assert(!contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < -10; }));
+    lean_assert(eqp(s1, s1));
+    sexpr s3 = s1;
+    lean_assert(eqp(s1, s3));
+    lean_assert(!eqp(sexpr(1), sexpr(1)));
 }
 
 static void tst2() {