From 52c4133021b06d33388895bc57785c497ac4a0e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2015 09:58:45 -0700
Subject: [PATCH] test(tests/shared/name.c): add anonymous unique test

---
 src/tests/shared/name.c | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/tests/shared/name.c b/src/tests/shared/name.c
index bfbffccb7..b5c15f2f3 100644
--- a/src/tests/shared/name.c
+++ b/src/tests/shared/name.c
@@ -9,6 +9,17 @@ void check(int v) {
     }
 }
 
+void anonymous_unique() {
+    lean_exception ex;
+    lean_name a1, a2;
+    check(lean_mk_anonymous_name(&a1, &ex));
+    check(lean_mk_anonymous_name(&a2, &ex));
+    check(lean_name_eq(a1, a2));
+    lean_del_name(a1);
+    lean_del_name(a2);
+    lean_del_exception(ex);
+}
+
 int main() {
     lean_exception ex;
     lean_name a, n1, n2, n3, n4, n5;
@@ -37,6 +48,7 @@ int main() {
     check(!lean_get_name_prefix(a, &n5, &ex));
     s3 = lean_get_exception_message(ex);
     printf("Lean exception: %s\n", s3);
+    anonymous_unique();
     lean_del_name(a);
     lean_del_name(n1);
     lean_del_name(n2);