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 *)
I don't understand, is hnf calling simpl under the hood?
This seems to indicate yes:
let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, )
IIRC it "calls"
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: Jun 09 2023 at 07:01 UTC