diff --git a/tests/lean/moduleDoc.lean b/tests/lean/moduleDoc.lean index 0c0dcd6e5f..1f38287f57 100644 --- a/tests/lean/moduleDoc.lean +++ b/tests/lean/moduleDoc.lean @@ -8,6 +8,14 @@ def tst : MetaM Unit := do let docs := getMainModuleDoc (← getEnv) IO.println <| docs.toList.map repr +def printDoc (moduleName : Name) : MetaM Unit := do + match getModuleDoc? (← getEnv) moduleName with + | some docs => IO.println <| docs.toList.map repr + | _ => throwError "module not found" + /-! Another module doc. -/ #eval tst + +#eval printDoc `Lean.Meta.ReduceEval +#eval printDoc `Lean.Data.Lsp.Communication diff --git a/tests/lean/moduleDoc.lean.expected.out b/tests/lean/moduleDoc.lean.expected.out index 79dcec68aa..7013b365ba 100644 --- a/tests/lean/moduleDoc.lean.expected.out +++ b/tests/lean/moduleDoc.lean.expected.out @@ -1 +1,3 @@ ["Testing module documentation. ", "Another module doc. "] +["Evaluation by reduction "] +["Reading/writing LSP messages from/to IO handles. "]