Hello,
Side effects are bad, but I'm in the following situation
let foo .... :=
let fix bar ... (fun_aux : ....) :=...
end in let fix foo_aux ... := ...
end in bar .... foo_aux.
i.e., the function bar
takes foo_aux
as a parameter.
foo_aux
is actually used only once while executing foo
but I would like to know how many times it is unfolded as a fixpoint.
I would like to avoid introducing an extra-parameter just for that purpose, because I would need to modify foo
(Coq seemingly cannot infer the type of fun_aux
if I do not specify it explicitly).
In practice, for the examples I'm considering, foo_aux
should be unfolded less thant 10 times, so that would be great to just print "unfold foo_aux" each time it is unfolded
what evaluation strategy?
look into https://github.com/coq-community/reduction-effects/ i guess
Cbv and cbn but I don't think it matter that much.
Thanks !
Last updated: Oct 13 2024 at 01:02 UTC