Janno (Oct 30 2020 at 12:29): Janno (Oct 30 2020 at 12:29):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.
Gaëtan Gilbert (Oct 30 2020 at 12:31):only full reduction afaik
Janno (Oct 30 2020 at 12:32):That's too bad. It's very useful :)
Gaëtan Gilbert (Oct 30 2020 at 12:40):make a PR to expose it
Pierre-Marie Pédrot (Oct 30 2020 at 12:43):in master it does
Pierre-Marie Pédrot (Oct 30 2020 at 12:44):ah, sorry, misunderstood what you meant, I thought you talked about the ML tactic api
Janno (Oct 30 2020 at 12:48):What I really want is to have it in ltac2. Pretyping and hnf are the main source of slowdown in my experiments right now :)
Janno (Oct 30 2020 at 12:48):I suppose this is a good opportunity to try to write a plugin that exposes this function
Pierre-Marie Pédrot (Oct 30 2020 at 12:49):FTR hnf is the dreaded whd-something-something-but-fix function we discussed about
Pierre-Marie Pédrot (Oct 30 2020 at 12:49):at least the ML API is truthful, which is not the case of the user-facing reduction function name
Janno (Oct 30 2020 at 12:52):Yes, I noticed that in the perf profile.. the name really is quite misleading
Janno (Oct 30 2020 at 12:53):The user-facing name, that is
Pierre-Marie Pédrot (Oct 30 2020 at 12:53):IIRC it goes back to the prehistory of Coq
Last updated: Dec 01 2023 at 06:01 UTC