Stream: Coq devs & plugin devs

Topic: hnf and simpl never


view this post on Zulip Hugo Herbelin (Feb 10 2022 at 12:31):

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 *)

view this post on Zulip Ali Caglayan (Feb 10 2022 at 13:26):

*deleted

view this post on Zulip Ali Caglayan (Feb 10 2022 at 13:29):

I don't understand, is hnf calling simpl under the hood?

view this post on Zulip Enrico Tassi (Feb 10 2022 at 13:29):

no

view this post on Zulip Ali Caglayan (Feb 10 2022 at 13:29):

This seems to indicate yes: let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])

view this post on Zulip Enrico Tassi (Feb 10 2022 at 13:29):

IIRC it "calls" cbn

view this post on Zulip Pierre-Marie Pédrot (Feb 10 2022 at 13:53):

This is simpl, not cbn. But it does not use the same exact flags

view this post on Zulip Hugo Herbelin (Feb 10 2022 at 14:58):

But the doc is wrong, right?

view this post on Zulip Hugo Herbelin (Feb 17 2022 at 16:19):

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