max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: doc string

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-30 11:27:09 -07:00
parent db5df69db4
commit 837677cb4c
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/printDecls.lean
View file

@ -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