## Stream: general

### Topic: apply_rules vs solve_by_elim

#### Johan Commelin (May 15 2020 at 19:22):

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 (May 16 2020 at 02:28):

apply_rules doesn't do any backtracking.

#### Scott Morrison (May 16 2020 at 02:28):

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 (May 16 2020 at 02:30):

(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 (May 16 2020 at 02:30):

We should add some doc-strings to this effect!

#### Johan Commelin (May 16 2020 at 03:42):

@Scott Morrison Aha, thx for explaining

#### Scott Morrison (May 16 2020 at 07:30):

#2696

Last updated: May 14 2021 at 22:15 UTC