Skip to content

Add `by` parameter to `multiset_solver`

Robbert Krebbers requested to merge robbert/multiset_solver_by into master

The tactics naive_solver and set_solver have a by parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to multiset_solver too, and similar to naive_solver/set_solver lets it default to eauto.

I cannot easily come up with useful test cases where we need the full power of eauto. Either just fast_done is sufficient (e.g., if the goal is an equality, see test_goal_{1,2} and gmultiset_singleton_subseteq) or you need eauto with some hints (see test_goal_3). Nonetheless, I think it makes sense to be consistent with naive_solver/set_solver to avoid issues such as !420 (merged).

Merge request reports