Probably a silly question, but I was wondering if it would be possible to print an expression at runtime, similar to Haskell's trace function.
This package reduction-effects might fit the bill: https://github.com/coq-community/reduction-effects
this looks right, but doesn't work for me : / I guess the project I am working in is non-trivial enough that it sidesteps something from this library.
It might be worth submitting a bug report if you can somehow minimize it.
Can you elaborate a bit more what doesn't work? I remember that I had the problem that just nothing happened as well at some point, but either I moved the
From ReductionEffect Require Import PrintingEffect. around or I put
Declare ML Module "redeffect_plugin". in the file where I wanted to use the effects. One of those fixed the problem for me, although I didn't understand why
Last updated: Jan 27 2023 at 00:03 UTC