Quentin VERMANDE (Oct 24 2023 at 14:29): Quentin VERMANDE (Oct 24 2023 at 14:29):If I may reopen this, I will really need to solve canonical structure instanciation using coq-elpi. But for this, I need a "hook" similar to what has been done for coercions. However, I have no idea how I should go about it. Could someone help me doing that?
Cyril Cohen (Oct 24 2023 at 14:31):Then it's a different topic than Typeclass instanciation :wink:
Notification Bot (Oct 24 2023 at 14:33):2 messages were moved here from #Elpi users & devs > Typeclass instanciation via elpi by Cyril Cohen.
Cyril Cohen (Oct 24 2023 at 14:37):Also, part of this topic should go to the #Coq devs & plugin devs stream.
Last updated: Oct 13 2024 at 01:02 UTC