Hi all,
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 : core
but as these are not Hint Rewrite
these should not be included, right?debug autorewrite
like you would debug debug auto
, but I could not find anything. Does this exist?Last updated: Oct 13 2024 at 01:02 UTC