mathlib
259c951d - doc(src/deprecated/*): add module docstrings (#14224)

Commit
3 years ago
doc(src/deprecated/*): add module docstrings (#14224) Although we don't ever import them now, I add module docstrings for a couple of deprecated files to make the linter happier. I also attempt to unify the style in the docstrings of all the deprecated files.
Author
Parents
Loading