Skip to content
Snippets Groups Projects

Add `by` parameter to `multiset_solver`

Merged 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading