From accdededc0f78e648b2eede1e556d0cda3e14b41 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Aug 2021 13:54:56 -0700
Subject: [PATCH] test: module docs

---
 tests/lean/moduleDoc.lean              | 13 +++++++++++++
 tests/lean/moduleDoc.lean.expected.out |  1 +
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/moduleDoc.lean
 create mode 100644 tests/lean/moduleDoc.lean.expected.out

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. "]