mathlib
8a7b94fb - chore(tactic/suggest): add a docstring (#2499)

Commit

5 years ago

chore(tactic/suggest): add a docstring (#2499) Co-authored-by: Scott Morrison <scott@tqft.net>

References

Author

khoek

Parents