Does Coq expose CClosure.whd_stack
as a reduction/tactic? I only realized just now that hnf
is not the right thing because it does too much.
only full reduction afaik
That's too bad. It's very useful :)
make a PR to expose it
in master it does
ah, sorry, misunderstood what you meant, I thought you talked about the ML tactic api
What I really want is to have it in ltac2. Pretyping and hnf
are the main source of slowdown in my experiments right now :)
I suppose this is a good opportunity to try to write a plugin that exposes this function
FTR hnf
is the dreaded whd-something-something-but-fix function we discussed about
at least the ML API is truthful, which is not the case of the user-facing reduction function name
Yes, I noticed that in the perf profile.. the name really is quite misleading
The user-facing name, that is
IIRC it goes back to the prehistory of Coq
Last updated: Dec 01 2023 at 06:01 UTC