diff --git a/tests/lean/moduleDoc.lean b/tests/lean/moduleDoc.lean
new file mode 100644
index 0000000000..0c0dcd6e5f
--- /dev/null
+++ b/tests/lean/moduleDoc.lean
@@ -0,0 +1,13 @@
+import Lean
+
+/-! Testing module documentation. -/
+
+open Lean
+
+def tst : MetaM Unit := do
+  let docs := getMainModuleDoc (← getEnv)
+  IO.println <| docs.toList.map repr
+
+/-! Another module doc. -/
+
+#eval tst
diff --git a/tests/lean/moduleDoc.lean.expected.out b/tests/lean/moduleDoc.lean.expected.out
new file mode 100644
index 0000000000..79dcec68aa
--- /dev/null
+++ b/tests/lean/moduleDoc.lean.expected.out
@@ -0,0 +1 @@
+["Testing module documentation. ", "Another module doc. "]