Stream: Hierarchy Builder devs & users

Topic: What does #[hnf] do?


view this post on Zulip Ali Caglayan (Sep 02 2021 at 14:15):

What does #[hnf] do?

view this post on Zulip Enrico Tassi (Sep 02 2021 at 14:51):

it's like Definition ... := Eval hnf in term, I did forget to document it

view this post on Zulip 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

view this post on Zulip 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: Nov 29 2023 at 04:01 UTC