apply_rules vs solve_by_elim

Stream: general

[Johan Commelin]

Do I understand correctly that apply_rules and solve_by_elim are somewhat similar? Is the idea that apply_rules is some sort of solve_by_elim only [...]? And solve_by_elim comes with a default set of rules, but apply_rules doesn't?

[Scott Morrison]

apply_rules doesn't do any backtracking.

[Scott Morrison]

Once a lemma has been applied on a particular goal, it won't go back to try other lemmas on that goal if it fails to discharge subsequent subgoals.

[Scott Morrison]

(And of course this brings an advantage: it can succeed without discharging all the subgoals, whereas solve_by_elim is a finishing tactic.)

[Scott Morrison]

We should add some doc-strings to this effect!

[Johan Commelin]

@Scott Morrison Aha, thx for explaining

[Scott Morrison]

#2696