What does #[hnf] do?
it's like 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: Nov 29 2023 at 04:01 UTC