lean#212 renaming tactic combinators

Stream: PR reviews

[Gabriel Ebner]

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]

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

[Reid Barton]

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]

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.