Zulip Chat Archive

Stream: PR reviews

Topic: lean#212 renaming tactic combinators


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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