The doc says that simpl never
applies to hnf
? Has it ever be the case?
Arguments id : simpl never.
Goal id (nat->nat).
hnf. (* nat -> nat *)
*deleted
I don't understand, is hnf calling simpl under the hood?
no
This seems to indicate yes: let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
IIRC it "calls" cbn
This is simpl, not cbn. But it does not use the same exact flags
But the doc is wrong, right?
In practise then, hnf
depends a little bit on simpl never
. @gares: do you remember whether the original intent was that hnf
depends on simpl never
or the contrary? In both cases, I believe we can implement the original intent.
Last updated: Oct 13 2024 at 01:02 UTC