This seems like an almost ridiculous limitation of
firstorder that came up in the CoqHammer authors' evaluation of his tactics against
firstorder, we did not implement iterative deepening, because the depth limit is a global parameter not changeable at the tactic language level
Shouldn't tactic-level depth limit be quite easy to implement?
Sure, that should be doable.
sounds good. However, since I'm not super invested in this topic myself, maybe I can just open an issue on it and say "this would be nice to have"?
Last updated: Feb 01 2023 at 15:04 UTC