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

test: check stdlib doc strings

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-10 07:36:16 -08:00
parent ac77df82c0
commit ac4961fa37
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/docStr.lean
View file

@ -67,5 +67,8 @@ def printDocStrings : MetaM Unit := do
printDocString `f.foo
printDocString `g
printDocString `g.foo
printDocString `optParam
printDocString `namedPattern
printDocString `Lean.Meta.forallTelescopeReducing
#eval printDocStrings

3
tests/lean/docStr.lean.expected.out
View file

@ -15,3 +15,6 @@ doc string for 'f' is not available
"let rec documentation at f "
doc string for 'g' is not available
"let rec documentation at g "
"Gadget for optional parameter support. "
"Auxiliary Declaration used to implement the named patterns `x@p` "
"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\n it reduces `A` and continues bulding the telescope if it is a `forall`. "