set_solver tactic roughly calls
set_unfold and then performs
naive_solver. @jihgfee noticed that
set_solver (without tactic argument) calls
naive_solver idtac by default. This is somewhat strange since
naive_solver (without tactic argument) defaults to
Also @jihgfee found an example where
set_solver by idtac (the current default) is much slower than
set_solver by eauto.
So I am wondering what's the reason why
idtac? Is that just some arbitrary legacy choice, or does it actually improve performance?