From e45211f31cfd5c8a18a2cfed8f53ccaf0708ee92 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Nov 2019 18:00:31 -0800
Subject: [PATCH] test: display discrimination tree containing type class
 instances

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

diff --git a/tests/lean/run/instances.lean b/tests/lean/run/instances.lean
new file mode 100644
index 0000000000..17b10de65c
--- /dev/null
+++ b/tests/lean/run/instances.lean
@@ -0,0 +1,12 @@
+import Init.Lean
+open Lean
+open Lean.Meta
+
+def tst1 : IO Unit :=
+do let mods := [`Init.Lean];
+   env ← importModules $ mods.map $ fun m => {module := m};
+   let insts := getInstances env;
+   IO.println (format insts);
+   pure ()
+
+#eval tst1