From 7607a244697cf8ae3ff613a10eea15ab6c9e81c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Sep 2021 17:47:23 -0700
Subject: [PATCH] test: `deriving DecidableEq` for enum types

Forgot to add test.
---
 tests/lean/run/enumDecEq.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/lean/run/enumDecEq.lean

diff --git a/tests/lean/run/enumDecEq.lean b/tests/lean/run/enumDecEq.lean
new file mode 100644
index 0000000000..0aece8c984
--- /dev/null
+++ b/tests/lean/run/enumDecEq.lean
@@ -0,0 +1,29 @@
+inductive Foo1 where
+  | a1
+  deriving DecidableEq
+
+#print Foo1.ofNat
+
+inductive Foo2 where
+  | a1 | a2
+  deriving DecidableEq
+
+#print Foo2.ofNat
+
+inductive Foo3 where
+  | a1 | a2 | a3
+  deriving DecidableEq
+
+#print Foo3.ofNat
+
+inductive Foo4 where
+  | a1 | a2 | a3 | a4
+  deriving DecidableEq
+
+#print Foo4.ofNat
+
+inductive Foo5 where
+  | a1 | a2 | a3 | a4 | a5
+  deriving DecidableEq
+
+#print Foo5.ofNat