Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: restore the module docstring code snippet (#7030)
We had this in mathlib3, allowing one to type `mo` (then press tab, at least for me) in an empty file and have a snippet template of a module docstring inserted with the title named to the filename, which can save a little time. The implementation is now a bit overkill as it splits on `_` and capitalizes still to get from the filename to the module title, which likely has no affect for most lean 4 filenames.
- Loading branch information