Sam Stites (Jun 02 2021 at 00:53): Sam Stites (Jun 02 2021 at 00:53):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.
Li-yao (Jun 02 2021 at 12:11):This package reduction-effects might fit the bill: https://github.com/coq-community/reduction-effects
Sam Stites (Jun 02 2021 at 13:55):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.
Li-yao (Jun 02 2021 at 14:21):It might be worth submitting a bug report if you can somehow minimize it.
Yannick Forster (Jun 03 2021 at 07:24):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: Oct 13 2024 at 01:02 UTC