From b7be3ec6de166001a49f45d5ee2414cce110dea3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Jan 2016 16:18:39 -0800
Subject: [PATCH] test(tests/lean/run): add tests for heterogeneous congruence
 lemma generator

---
 tests/lean/run/hcongr_1.lean | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 tests/lean/run/hcongr_1.lean

diff --git a/tests/lean/run/hcongr_1.lean b/tests/lean/run/hcongr_1.lean
new file mode 100644
index 0000000000..f50943e295
--- /dev/null
+++ b/tests/lean/run/hcongr_1.lean
@@ -0,0 +1,6 @@
+import data.tuple
+
+#hcongr @tuple.append
+#hcongr @add
+#hcongr @list.ith
+#hcongr (@list.ith nat)