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