I have a rule for autorewrite that is very slow, even when it is the only rule given to autorewrite. This singular hint does the opposite of what simpl does, so doing
repeat(tactic; simpl) will loop forever. The weird thing is that when I run autorewrite with all my hints it takes a long time, but it does end up with the right answer. How do I debug this?
simpl(which will cause it to loop)? I have added a bunch of stuff to core using
Hint Resolve foo : corebut as these are not
Hint Rewritethese should not be included, right?
debug autorewritelike you would debug
debug auto, but I could not find anything. Does this exist?
Last updated: Oct 03 2023 at 20:01 UTC