mathlib3
b0552c15 - docs(tactic/lint/default): Module docstring (#13570)

Commit

3 years ago

docs(tactic/lint/default): Module docstring (#13570) Write the module docstring.

Author

YaelDillies

YaelDillies

Parents

Loading