## Stream: PR reviews

### Topic: lean#212 renaming tactic combinators

#### Gabriel Ebner (May 05 2020 at 09:46):

What do you think of renaming all_goals to all_goals'? (And changing all_goals so that it returns the results of the tactics.) I'm not sure I see the motivation behind the change, consistency aside. If we don't want to rename the existing combinators, then IMHO we could just add the new ones to mathlib directly.

#### Reid Barton (May 05 2020 at 11:16):

If you use a tactic that returns a result (other than unit) interactively, is the result just silently discarded?

#### Reid Barton (May 05 2020 at 11:18):

In principle for things like mmap/mmap' it's usually more efficient to discard the results, but I think that can't make a measurable difference in the case of all_goals...

#### Reid Barton (May 05 2020 at 11:18):

What about this argument: tactic.interactive.all_goals is for interactive use, and for interactive use you would never want to use the results (right?) so it should discard them.

Last updated: May 06 2021 at 12:15 UTC