It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of reduction-effects for cbv (alas, no support for native_compute / vm_compute, yet; see rocq-community/reduction-effects#8) and using extraction directives for OCaml/Haskell, to insert debug print calls in the main loop of the rewriter, to thread through and print out some sort of debugging information, with minimal overhead when we're not printing debug info.
It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of reduction-effects for
cbv(alas, no support fornative_compute/vm_compute, yet; see rocq-community/reduction-effects#8) and using extraction directives for OCaml/Haskell, to insert debug print calls in the main loop of the rewriter, to thread through and print out some sort of debugging information, with minimal overhead when we're not printing debug info.