Stream: Coq devs & plugin devs

Topic: whd_nored?

view this post on Zulip Gaëtan Gilbert (Sep 29 2021 at 15:13):

What does Reductionops.whd_nored do?

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2021 at 15:14):

Nothing but the stack variant is used to extract the head of a KAM process

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2021 at 15:15):

(it does remove the head casts and expand metas / evars though, so it's not exactly the identity)

Last updated: Feb 06 2023 at 00:03 UTC