mathlib
51696a64
- chore(data/analysis/*): Fix lint and docs (#16751)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(data/analysis/*): Fix lint and docs (#16751) Write the missing docstrings and module docs for `data.analysis.filter` and `data.analysis.topology`. Satisfy the `has_nonempty_instance` and `unused_arguments` linters.
Author
YaelDillies
Parents
2bb1bae8
Loading