From 837677cb4cf7676fd3a8fa8fc604a2a2931869e5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Sep 2021 11:27:09 -0700 Subject: [PATCH] test: doc string --- tests/lean/run/printDecls.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/lean/run/printDecls.lean b/tests/lean/run/printDecls.lean index 81635a13c4..b6b4ddf41d 100644 --- a/tests/lean/run/printDecls.lean +++ b/tests/lean/run/printDecls.lean @@ -15,8 +15,12 @@ def printDecls (pre : Name) : MetaM Unit := do let cs := (← getEnv).constants cs.forM fun declName info => do if pre.isPrefixOf declName && !shouldIgnore declName then - IO.println s!"{declName} : {← ppExpr info.type}" + if let some docString := findDocString? (← getEnv) declName then + IO.println s!"/-- {docString} -/\n{declName} : {← ppExpr info.type}" + else + IO.println s!"{declName} : {← ppExpr info.type}" #eval printDecls `Array #eval printDecls `List #eval printDecls `Bool +#eval printDecls `Lean.Elab