## Stream: PR reviews

### Topic: lean#296 mention tactics in docstrings

#### Johan Commelin (Jul 14 2020 at 06:25):

I think we should try to do something with this PR. I don't really care if we do this in core or in mathlib. But it would be great to have docstrings on forall and exists that tell the user which tactics to use.

Last updated: May 06 2021 at 13:21 UTC