This seems like an almost ridiculous limitation of firstorder
that came up in the CoqHammer authors' evaluation of his tactics against firstorder
:
For
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: Oct 13 2024 at 01:02 UTC