Stream: Coq devs & plugin devs

Topic: reduce_to_ind_gen hnf?

view this post on Zulip Gaëtan Gilbert (Sep 09 2021 at 09:19):

Anyone know why reduce_to_ind_gen use the tacred reduction hnf_constr?

view this post on Zulip Guillaume Melquiond (Sep 09 2021 at 09:36):

You mean: Instead of using whd_all? That is a good question.

view this post on Zulip Hugo Herbelin (Sep 10 2021 at 13:49):

Not sure. Doesn't hnf_constr better preserve the name of constants unfolding to a fix?

Last updated: Jun 13 2024 at 06:01 UTC