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? https://github.com/coq/coq/blob/4cb847934949e89a644a5dedb4306cd54d91096c/pretyping/tacred.ml#L1273

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: Oct 21 2021 at 21:03 UTC