Re: The solver does not terminate

On 06/12/2024 17:17, Julio Di Egidio wrote:

On 06/12/2024 16:58, Mild Shock wrote:

Cut away certain rules, avoiding even more backtracking.

 I had `once` initially, as that certainly makes sense, but it was failing even some of the simpler pos cases.  I shall try again.

Indeed, not even a plain `once` works since there may be more than one *different* matching hypothesis, and committing to the first one in order may lead to failure.
Anyway, as said, I'd rather not cut on the search space (at all), plus I don't see how cutting should matter to termination (given that the reduction rules are not recursive).
I need to think more about it: what is exactly going wrong.
-Julio