Repository navigation
TODO: Experiment with Hints in derive.v #2069
Description
@yosakaon made the following observation:
This is about the following hint:
Hint Extern 0 (is_derive _ _ (fun x => _ *m _) _) => apply: is_derive_mulmx : typeclass_instances.
Activity
yosakaon commentedon Jul 31, 2026
I don't know if it is the best course of action to add such a hint and if it might break (I don't think so) other developments but it works well in my current development. I can open a PR but I'd like to know if there is any "canonical" way to deal with such a problem (simple apply fails in harder goals -> use
apply:). But unless this hint is in place afaik, typeclass inference will fail at solving such goals, which fails the objective of usingis_derivein the first place and rendersis_derive_mulmxpointless.yosakaon commentedon Jul 31, 2026
eapply is_derive_mulmxworks as well in a compound goal.affeldt-aist commentedon Aug 30, 2026
Since PR #2017 seems inconclusive, shall we close this issue? (fyi: @CohenCyril )
affeldt-aist commentedon Sep 2, 2026
ping @yosakaon
yosakaon commentedon Sep 2, 2026
I think it's ok to close
affeldt-aist commentedon Sep 2, 2026
Thanks!