What does #[hnf] do?
Definition ... := Eval hnf in term, I did forget to document it
but it does the hnf for each canonical instance it builds, not for the actual term you give to HB.instance
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: Jan 29 2023 at 14:02 UTC