Stream: Coq devs & plugin devs

Topic: hnf and simpl never

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

Ali Caglayan (Feb 10 2022 at 13:26):

*deleted

Ali Caglayan (Feb 10 2022 at 13:29):

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

Enrico Tassi (Feb 10 2022 at 13:29):

no

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, [])

Enrico Tassi (Feb 10 2022 at 13:29):

IIRC it "calls" cbn

Pierre-Marie Pédrot (Feb 10 2022 at 13:53):

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

Hugo Herbelin (Feb 10 2022 at 14:58):

But the doc is wrong, right?

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: Apr 16 2024 at 23:01 UTC