Ali Caglayan (Sep 02 2021 at 14:15): Ali Caglayan (Sep 02 2021 at 14:15):What does #[hnf] do?
Enrico Tassi (Sep 02 2021 at 14:51):it's like Definition ... := Eval hnf in term, I did forget to document it
Enrico Tassi (Sep 02 2021 at 14:52):but it does the hnf for each canonical instance it builds, not for the actual term you give to HB.instance
Enrico Tassi (Sep 02 2021 at 14:53):in mathcom there are a few Definition foo_eqMixin := Eval hnf in term and it turns out this hnf is crucial for extraspecial.v and extremal.v. We had to tweak a nasty kernel flag before to make them pass without the hnf.
Last updated: May 28 2023 at 18:29 UTC